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.
---
 printing/printer.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index bb54f587fd..97e0528939 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -490,8 +490,8 @@ let pr_concl n ?(diffs=false) ?og_s sigma g =
   header ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
-let pr_evgl_sign sigma evi =
-  let env = evar_env evi in
+let pr_evgl_sign env sigma evi =
+  let env = evar_env env evi in
   let ps = pr_named_context_of env sigma in
   let _, l = match Filter.repr (evar_filter evi) with
   | None -> [], []
@@ -517,7 +517,8 @@ let pr_evgl_sign sigma evi =
 (* Print an existential variable *)
 
 let pr_evar sigma (evk, evi) =
-  let pegl = pr_evgl_sign sigma evi in
+  let env = Global.env () in
+  let pegl = pr_evgl_sign env sigma evi in
   hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
 
 (* Print an enumerated list of existential variables *)
-- 
cgit v1.2.3