diff --git a/src/prover/AC.ml b/src/prover/AC.ml
index d6245064d..6fd41ff47 100644
--- a/src/prover/AC.ml
+++ b/src/prover/AC.ml
@@ -242,7 +242,7 @@ module Make(Env : Env.S) : S with module Env = Env = struct
     )
 
   let register_ac c id ty =
-    add (C.proof_parent c) id ty
+    add ~proof:(C.proof_parent c) id ty
 
   let scan_clause c =
     let exception Fail in
diff --git a/src/prover/clause.ml b/src/prover/clause.ml
index 790ea68ff..3bee0347c 100644
--- a/src/prover/clause.ml
+++ b/src/prover/clause.ml
@@ -111,7 +111,7 @@ module Make(Ctx : Ctx.S) : S with module Ctx = Ctx = struct
     (* create the structure *)
     let ord = Ctx.ord () in
     let max_lits = lazy ( BV.to_list @@ Lits.maxlits sclause.lits ~ord ) in
-    let rec c = {
+    let c = {
       sclause;
       penalty;
       selected;
diff --git a/src/prover/clauseQueue.ml b/src/prover/clauseQueue.ml
index 9c19eea9b..33fd6612e 100644
--- a/src/prover/clauseQueue.ml
+++ b/src/prover/clauseQueue.ml
@@ -386,7 +386,7 @@ module Make(C : Clause_intf.S) = struct
             w_diff_l args1 args2
           | T.Fun(ty1, body1), T.Fun(ty2, body2) 
             when Type.equal ty1 ty2 && Type.equal (T.ty body1) (T.ty body2) ->
-            w_diff body1 body2
+            w_diff ~given_term:body1 ~conj_term:body2
           | _, _ -> 
             int_of_float (inst_penalty *. (w conj_term) +. gen_penalty *. (w given_term))
         and w_diff_l xs ys =
diff --git a/src/prover/env.ml b/src/prover/env.ml
index c61dd7dae..56541434e 100644
--- a/src/prover/env.ml
+++ b/src/prover/env.ml
@@ -806,7 +806,7 @@ module Make(X : sig
       match rules with
       | [] -> None
       | r :: rs ->
-        CCOpt.or_lazy ~else_:(fun () -> apply_rules rs c) (r c) in
+        CCOpt.or_lazy ~else_:(fun () -> apply_rules ~rules:rs c) (r c) in
     
     let q = Queue.create () in
     Queue.add c q;
diff --git a/src/prover/eprover_interface.ml b/src/prover/eprover_interface.ml
index d67b05532..dd4206292 100644
--- a/src/prover/eprover_interface.ml
+++ b/src/prover/eprover_interface.ml
@@ -57,7 +57,7 @@ module Make(E : Env.S) : S with module Env = E = struct
   let output_empty_conj ~out =
     Format.fprintf out "thf(conj,conjecture,($false))."
 
-  let rec encode_ty_args_t ~encoded_symbols t =
+  let encode_ty_args_t ~encoded_symbols t =
     let make_new_sym mono_head =
       if not (T.is_ground mono_head) then (
          let err = 
diff --git a/src/prover_calculi/Higher_order.ml b/src/prover_calculi/Higher_order.ml
index 699f6cd2e..7bab6326b 100644
--- a/src/prover_calculi/Higher_order.ml
+++ b/src/prover_calculi/Higher_order.ml
@@ -1719,9 +1719,9 @@ module Make(E : Env.S) : S with module Env = E = struct
               when Type.is_var (T.ty t) && not is_poly_arg_cong_res ->
               (* A polymorphic variable might be functional on the ground level *)
               let ty_args = 
-                OSeq.iterate [Type.var @@ HVar.fresh ~ty:Type.tType ()] 
-                  (fun types_w -> 
-                    Type.var (HVar.fresh ~ty:Type.tType ()) :: types_w) in
+                OSeq.iterate (fun types_w ->
+                    Type.var (HVar.fresh ~ty:Type.tType ()) :: types_w)
+                  [Type.var @@ HVar.fresh ~ty:Type.tType ()] in
               let res = 
                 ty_args
                 |> OSeq.mapi (fun arrarg_idx arrow_args ->
diff --git a/src/prover_calculi/app_encode.ml b/src/prover_calculi/app_encode.ml
index 6963a86a4..9d3212cb6 100644
--- a/src/prover_calculi/app_encode.ml
+++ b/src/prover_calculi/app_encode.ml
@@ -151,7 +151,7 @@ let rec app_encode_term toplevel t  =
 (** Encode a literal *)
 let app_encode_lit lit = 
   Util.debugf ~section 2 "# Encoding Literal %a" (fun k -> k (SLiteral.pp T.pp) lit);
-  SLiteral.map (app_encode_term true) lit
+  SLiteral.map ~f:(app_encode_term true) lit
 
 (** Encode a clause *)
 let app_encode_lits lits = List.map app_encode_lit lits
@@ -257,4 +257,4 @@ let options =
 
 let () =
   Options.add_opts
-    [ "--app-encode", Arg.Symbol (List.map fst options, fun o -> mode_ := List.assoc o options), " enable applicative encoding"]
\ No newline at end of file
+    [ "--app-encode", Arg.Symbol (List.map fst options, fun o -> mode_ := List.assoc o options), " enable applicative encoding"]
diff --git a/src/prover_calculi/bool_encode.ml b/src/prover_calculi/bool_encode.ml
index 28767bb63..b064ed1f1 100644
--- a/src/prover_calculi/bool_encode.ml
+++ b/src/prover_calculi/bool_encode.ml
@@ -325,7 +325,7 @@ let bool_encode_lit lit =
     assert(T.equal (T.ty_exn true_term) (T.ty_exn encoded_atom));
     mk_equ_lit (bool_encode_term atom) true_term
   | Eq _ | Neq _ ->
-    SLiteral.map bool_encode_term lit
+    SLiteral.map ~f:bool_encode_term lit
 
 (** Encode a clause *)
 let bool_encode_lits lits = List.map bool_encode_lit lits
@@ -413,4 +413,4 @@ let extension =
 
 let () =
   Options.add_opts
-    [ "--encode-booleans", Arg.Bool ((:=) enabled_), " enable encoding of booleans into a fresh type"]
\ No newline at end of file
+    [ "--encode-booleans", Arg.Bool ((:=) enabled_), " enable encoding of booleans into a fresh type"]
diff --git a/src/prover_calculi/lazy_cnf.ml b/src/prover_calculi/lazy_cnf.ml
index 8d2d3107a..c3ed4a13a 100644
--- a/src/prover_calculi/lazy_cnf.ml
+++ b/src/prover_calculi/lazy_cnf.ml
@@ -131,7 +131,7 @@ module Make(E : Env.S) : S with module Env = E = struct
 
       let arg_combinations = CCList.cartesian_product arg_ms in
       let arg_comb_num = List.fold_left (fun acc a -> acc * (List.length a)) 1 arg_ms in
-      let fun_table = CCArray.create arg_comb_num (List.hd ret_m) in
+      let fun_table = CCArray.make arg_comb_num (List.hd ret_m) in
 
       let iter_funs () = 
         let rec aux i k =
diff --git a/tests/testMultiset.ml b/tests/testMultiset.ml
index f7e427e03..9085c3a1f 100755
--- a/tests/testMultiset.ml
+++ b/tests/testMultiset.ml
@@ -4,7 +4,7 @@ module Q = QCheck
 
 module M = Multiset.Make(struct
   type t = int
-  let compare i j=Pervasives.compare i j
+  let compare i j=Stdlib.compare i j
 end)
 
 (* for testing *)
@@ -146,7 +146,7 @@ let max_is_max =
   let gen = Q.(map M.of_list (list small_int)) in
   let gen = Q.set_print pp gen in
   let prop m =
-    let f x y = Comparison.of_total (Pervasives.compare x y) in
+    let f x y = Comparison.of_total (Stdlib.compare x y) in
     let l = M.max f m |> M.to_list |> List.map fst in
     List.for_all (fun x -> M.is_max f x m) l
   in
diff --git a/tests/testTerm.ml b/tests/testTerm.ml
index dea1dc597..42f8cc109 100755
--- a/tests/testTerm.ml
+++ b/tests/testTerm.ml
@@ -110,7 +110,7 @@ let test_whnf2 = "whnf2", `Quick, fun () ->
   Alcotest.(check t_test) "whnf2" t1 t';
   ()
 
-let test_whnf2 = "patterns", `Quick, fun () ->
+let test_patterns = "patterns", `Quick, fun () ->
   let t1 = f (g a) (g b) in 
   let t2 = T.fun_ ty (f (T.bvar ~ty 0) (g (T.bvar ~ty 1))) in
   let t3 = T.fun_ ty (f (fun_var (T.bvar ~ty 0) (T.bvar ~ty 1)) (g (T.bvar ~ty 1))) in 
@@ -207,6 +207,7 @@ let suite : unit Alcotest.test_case list =
     test_app_var;
     test_whnf1;
     test_whnf2;
+    test_patterns;
     test_polymorphic_app;
     test_eta_reduce;
     test_eta_expand;