diff options
| author | Pierre-Marie Pédrot | 2019-12-24 14:19:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-26 12:42:31 +0100 |
| commit | 9d0e4b2ab78b89e39c63e8010ffd03745b309b5a (patch) | |
| tree | 98bbde69fba3fb77d2d7705c55cfbed781570368 /engine/proofview.ml | |
| parent | feea1d0377e2fb083efe74cd241e7867d008d5be (diff) | |
Remove uses of Global in Evd API.
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 6f8e668e4e..16be96454e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1039,9 +1039,9 @@ let (>>=) = tclBIND (** {6 Goal-dependent tactics} *) -let goal_env evars gl = +let goal_env env evars gl = let evi = Evd.find evars gl in - Evd.evar_filtered_env evi + Evd.evar_filtered_env env evi let goal_nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -1256,9 +1256,10 @@ module V82 = struct let of_tactic t gls = try + let env = Global.env () in let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let name, poly = Names.Id.of_string "legacy_pe", false in - let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in + let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in |