From 7b1e94365bee6cc984e5f476864ac753e6f46e3a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
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.
---
 printing/printer.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 8469490f0..ac20eeb6f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,10 +28,7 @@ let delayed_emacs_cmd s =
   if !Flags.print_emacs then s () else str ""
 
 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)
+  Pfedit.get_current_context ()
 
 (**********************************************************************)
 (** Terms                                                             *)
-- 
cgit v1.2.3