env, sigma as first arguments of functions

1 files changed, 8 insertions, 8 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36785b15dd..e8c96b7cd9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1342,7 +1342,7 @@ module Search = struct
                                             | Some i -> str ", with depth limit " ++ int i));
     tac
 
-  let run_on_evars p evm tac env =
+  let run_on_evars env evm p tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
     | Some (goals, evm') ->
@@ -1374,22 +1374,22 @@ module Search = struct
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
-  let evars_eauto depth only_classes unique dep st hints p evd env =
+  let evars_eauto env evd depth only_classes unique dep st hints p =
     let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
-    let res = run_on_evars p evd eauto_tac env in
+    let res = run_on_evars env evd p eauto_tac in
     match res with
     | None -> evd
     | Some evd' -> evd'
 
-  let typeclasses_eauto ?depth unique st hints p evd env =
-    evars_eauto depth true unique false st hints p evd env
+  let typeclasses_eauto env evd ?depth unique st hints p =
+    evars_eauto env evd depth true unique false st hints p
   (** Typeclasses eauto is an eauto which tries to resolve only
       goals of typeclass type, and assumes that the initially selected
       evars in evd are independent of the rest of the evars *)
 
-  let typeclasses_resolve debug depth unique p evd env =
+  let typeclasses_resolve env evd debug depth unique p =
     let db = searchtable_map typeclasses_db in
-    typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd env
+    typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
 end
 
 (** Binding to either V85 or Search implementations. *)
@@ -1534,7 +1534,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
           if get_typeclasses_legacy_resolution () then
             V85.resolve_all_evars_once debug depth unique p evd
           else
-            Search.typeclasses_resolve debug depth unique p evd env
+            Search.typeclasses_resolve env evd debug depth unique p
         in
          if has_undefined p oevd evd' then raise Unresolved;
          docomp evd' comps