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.
---
 proofs/pfedit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs/pfedit.ml')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b635cc963..2f5c1d1c2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -85,7 +85,8 @@ let get_current_goal_context () =
   with NoSuchGoal ->
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
-    (Evd.empty, Global.env ())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
-- 
cgit v1.2.3