From 6810929f652be3ebe40de86fe360665c6aded049 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Jun 2011 18:43:33 +0000
Subject: Cleaning debugging printer relative to new proof engine. In
 particular, new printer for evar_map which displays undefined evars + defined
 evars that were instantiated by these undefined evars and recursively, up to
 some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/include         | 4 ----
 dev/top_printers.ml | 3 ++-
 2 files changed, 2 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/include b/dev/include
index 243f9ea5f5..1648d5791c 100644
--- a/dev/include
+++ b/dev/include
@@ -24,11 +24,7 @@
 #install_printer  (* judgement *) ppj;;
 
 #install_printer  (* hint_db *)  print_hint_db;;
-#install_printer  (* goal *)  ppgoal;;
-#install_printer  (* sigma goal *)  ppsigmagoal;;
-#install_printer  (* proof *)  pproof;;
 #install_printer  (* Goal.goal *)  ppgoalgoal;;
-#install_printer  (* pftreestate *)  pppftreestate;;
 #install_printer  (* metaset.t *) ppmetas;;
 #install_printer  (* evar_map *)  ppevm;;
 #install_printer  (* clenv *) ppclenv;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 547ca0475a..333cf1a67b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -112,7 +112,8 @@ let pp_transparent_state s = pp (pr_transparent_state s)
 
 (* proof printers *)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map evd)
+let ppevm evd = pp(pr_evar_map (Some 2) evd)
+let ppevmall evd = pp(pr_evar_map None evd)
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 (* spiwack: deactivated until a replacement is found
-- 
cgit v1.2.3