diff options
| author |  amblaf <you@example.com> | 2017-06-15 11:34:40 +0200 |
|---|---|---|
| committer | amblaf <you@example.com> | 2017-07-31 10:34:00 +0200 |
| commit | 7a56397ae26854df6335a3325353d0a5d6c894ea (patch) | |
| tree | 76b60550d291123d47497196e963dff7e2589498 /tactics/class_tactics.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
Remove references to Global.env in tactics/*.ml
Only in ml files that are not related to Coq commands
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fc2fc31b..36785b15d 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 p evm tac env = 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 depth only_classes unique dep st hints p evd env = 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 p evd eauto_tac env 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 ?depth unique st hints p evd env = + evars_eauto depth true unique false st hints p evd env (** 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 debug depth unique p evd env = let db = searchtable_map typeclasses_db in - typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd + typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd env 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 + Search.typeclasses_resolve debug depth unique p evd env in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps |