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/evd.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 94868d9bdd..8e7d942c37 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -200,13 +200,14 @@ let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
   in
   make_hyps filter (evar_context evi)
 
-let evar_env evi = Global.env_of_context evi.evar_hyps
+let evar_env env evi =
+  Environ.reset_with_named_context evi.evar_hyps env
 
-let evar_filtered_env evi = match Filter.repr (evar_filter evi) with
-| None -> evar_env evi
+let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
+| None -> evar_env env evi
 | Some filter ->
   let rec make_env filter ctxt = match filter, ctxt with
-  | [], [] -> reset_context (Global.env ())
+  | [], [] -> reset_context env
   | false :: filter, _ :: ctxt -> make_env filter ctxt
   | true :: filter, decl :: ctxt ->
     let env = make_env filter ctxt in
-- 
cgit v1.2.3