From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
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 ++-
 proofs/pfedit.ml    |  3 ++-
 stm/lemmas.ml       | 10 ++++++++--
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 63755d7ff7..4e740bffe2 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                                                             *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b635cc9632..2f5c1d1c2b 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
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f06abfcce7..fb64a10c6c 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -511,5 +511,11 @@ let save_proof ?proof = function
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+    try (* No more focused goals ? *)
+      let p = Pfedit.get_pftreestate () in
+      let evd = Proof.in_proof p (fun x -> x) in
+      (evd, Global.env ())
+    with Proof_global.NoCurrentProof ->
+      let env = Global.env () in
+      (Evd.from_env env, env)
+           
-- 
cgit v1.2.3