Merge PR #805: Functional tactics

1 files changed, 9 insertions, 9 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 371debede..b98b10315 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 =
+  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') ->
@@ -1357,7 +1357,7 @@ module Search = struct
        let pv = Proofview.unshelve goals pv in
        try
          let (), pv', (unsafe, shelved, gaveup), _ =
-           Proofview.apply (Global.env ()) tac pv
+           Proofview.apply env tac pv
          in
          if Proofview.finished pv' then
            let evm' = Proofview.return pv' in
@@ -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 =
+  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 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 =
-    evars_eauto depth true unique false st hints p evd
+  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 =
+  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
+    typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
 end
 
 (** Binding to either V85 or Search implementations. *)
@@ -1532,7 +1532,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
+            Search.typeclasses_resolve env evd debug depth unique p
         in
          if has_undefined p oevd evd' then raise Unresolved;
          docomp evd' comps