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.
---
 vernac/himsg.ml         | 4 ++--
 vernac/vernacentries.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 19ec0a3642..c8e308cb9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -605,7 +605,7 @@ let rec explain_evar_kind env sigma evk ty =
 let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr env sigma evi.evar_concl with
   | Some _ ->
-    let env = Evd.evar_filtered_env evi in
+    let env = Evd.evar_filtered_env env evi in
       fnl () ++ str "Could not find an instance for " ++
       pr_leconstr_env env sigma evi.evar_concl ++
       pr_trailing_ne_context_of env sigma
@@ -622,7 +622,7 @@ let explain_placeholder_kind env sigma c e =
 
 let explain_unsolvable_implicit env sigma evk explain =
   let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
-  let env = Evd.evar_filtered_env evi in
+  let env = Evd.evar_filtered_env env evi in
   let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
   let pe = pr_trailing_ne_context_of env sigma in
   strbrk "Cannot infer " ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 604d1b28ff..d3bc06cd6c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -474,7 +474,7 @@ let program_inference_hook env sigma ev =
   let tac = !Obligations.default_tactic in
   let evi = Evd.find sigma ev in
   let evi = Evarutil.nf_evar_info sigma evi in
-  let env = Evd.evar_filtered_env evi in
+  let env = Evd.evar_filtered_env env evi in
   try
     let concl = evi.Evd.evar_concl in
     if not (Evarutil.is_ground_env sigma env &&
-- 
cgit v1.2.3