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

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 7876e9a48f..8843adc853 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -125,8 +125,8 @@ val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
 val evar_candidates : evar_info -> constr list option
 val evar_filter : evar_info -> Filter.t
-val evar_env :  evar_info -> env
-val evar_filtered_env :  evar_info -> env
+val evar_env : env -> evar_info -> env
+val evar_filtered_env : env -> evar_info -> env
 
 val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
 val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
-- 
cgit v1.2.3