From 7b1e94365bee6cc984e5f476864ac753e6f46e3a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 May 2016 13:25:52 +0200
Subject: Pfedit.get_current_context refinement (fix #4523)

Return the most appropriate evar_map for commands that can run on
non-focused proofs (like Check, Show and debug printers) so that
universes and existentials are printed correctly (they are global
to the proof). The API is backwards compatible.
---
 stm/lemmas.ml  | 10 +---------
 stm/lemmas.mli |  1 -
 2 files changed, 1 insertion(+), 10 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index fb64a10c6c..5b205e79ef 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -509,13 +509,5 @@ let save_proof ?proof = function
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    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)
+  Pfedit.get_current_context ()
            
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 16e54e318e..ca6af9a3fa 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -60,4 +60,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
-
-- 
cgit v1.2.3