From 9d0e4b2ab78b89e39c63e8010ffd03745b309b5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Dec 2019 14:19:56 +0100
Subject: 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.
---
 engine/proofview.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'engine/proofview.ml')

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
-- 
cgit v1.2.3