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.
---
 proofs/evar_refiner.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/evar_refiner.ml')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 59918ab2f9..8297b11585 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -44,10 +44,10 @@ let define_and_solve_constraints evk c env evd =
     | Success evd -> evd
     | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
 
-let w_refine (evk,evi) (ltac_var,rawc) sigma =
+let w_refine (evk,evi) (ltac_var,rawc) env sigma =
   if Evd.is_defined sigma evk then
     user_err Pp.(str "Instantiate called on already-defined evar");
-  let env = Evd.evar_filtered_env evi in
+  let env = Evd.evar_filtered_env env evi in
   let sigma',typed_c =
     let flags = {
       Pretyping.use_typeclasses = true;
-- 
cgit v1.2.3