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.
---
 dev/top_printers.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6e5b048ccd..4c733dd4f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -485,9 +485,7 @@ let ppist ist =
 (* Vernac-level debugging commands                                    *)
 
 let in_current_context f c =
-  let (evmap,sign) =
-    try Pfedit.get_current_goal_context ()
-    with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
+  let (evmap,sign) = Pfedit.get_current_context () in
   f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
 (* We expand the result of preprocessing to be independent of camlp4
-- 
cgit v1.2.3


From 27dffdea5b46f6282c1584db0555213e744352fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 31 May 2016 13:33:01 +0200
Subject: Revert "Rename Lexer -> CLexer."

This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e.
---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index e054c1bc70..ad9a5d75e6 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -151,7 +151,7 @@ States
 
 Genprint
 Tok
-CLexer
+Lexer
 Ppextend
 Pputils
 Ppannotation
-- 
cgit v1.2.3