From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 25 Mar 2016 16:46:50 +0100
Subject: Univs: fix get_current_context (bug #4603, part I)

Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
---
 printing/printer.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 63755d7ff..4e740bffe 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -30,7 +30,8 @@ let delayed_emacs_cmd s =
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    (Evd.empty, Global.env())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 (**********************************************************************)
 (** Terms                                                             *)
-- 
cgit v1.2.3