From 012fe1a96ba81ab0a7fa210610e3f25187baaf1d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Aug 2014 14:03:32 +0200
Subject: Referring to evars by names. Added a parser for evars (but parsing of
 instances still to do). Using heuristics to name after the quantifier name it
 comes. Also added a "sigma" to almost all printing functions.

---
 dev/top_printers.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 56c71d88f5..4fedbec8e9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -200,8 +200,8 @@ let ppuniverse_context_future c =
 let ppuniverses u = pp (Univ.pr_universes u)
 
 let ppenv e = pp
-  (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
-   str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
+  (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
+   str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
 
 let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
 
@@ -457,7 +457,7 @@ 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
-  f (fst (Constrintern.interp_constr evmap sign c))(*FIXME*)
+  f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
 (* We expand the result of preprocessing to be independent of camlp4
 
-- 
cgit v1.2.3