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 ----
 1 file changed, 4 deletions(-)

(limited to 'dev/include')

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;;
-- 
cgit v1.2.3