From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 May 2018 17:44:34 +0200
Subject: Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.
---
 plugins/ltac/pptactic.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bd02d85d59..3dfe308a5d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) =
              let open Genprint in
              match generic_top_print (in_gen (Topwit wit) x) with
              | TopPrinterBasic pr -> pr ()
-             | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | TopPrinterNeedsContext pr ->
+               let env = Global.env() in
+               pr env (Evd.from_env env)
              | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-                printer (Global.env()) Evd.empty default_ensure_surrounded
+               let env = Global.env() in
+               printer env (Evd.from_env env) default_ensure_surrounded
           end
         | _ -> default
 
-- 
cgit v1.2.3