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
---
 proofs/clenv.ml   | 2 +-
 proofs/clenv.mli  | 2 +-
 proofs/goal.ml    | 3 ++-
 proofs/tacmach.ml | 4 ++--
 4 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 8c05499a2f..6e6fff96d1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -519,4 +519,4 @@ let pr_clenv clenv =
   h 0
     (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
      str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
-     pr_evar_map clenv.evd)
+     pr_evar_map (Some 2) clenv.evd)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b685f5041f..abd67236ac 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -134,6 +134,6 @@ val clenv_conv_leq :
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
-(** {6 Pretty-print } *)
+(** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9be2d028a1..0f10c7f84b 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Term
 
 (* This module implements the abstract interface to goals *)
@@ -22,7 +23,7 @@ type goal = {
 (* spiwack: I don't deal with the tags, yet. It is a worthy discussion
    whether we do want some tags displayed besides the goal or not. *)
 
-let pr_goal {content = e} = Pp.int e
+let pr_goal {content = e} = str "GOAL:" ++ Pp.int e
 
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5bfdba8a49..5475daa89f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -213,9 +213,9 @@ let db_pr_goal sigma g =
                    str" "  ++ pc) ++ fnl ()
 
 let pr_gls gls =
-  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
+  hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
 
 let pr_glls glls =
-  hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+  hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls))
 
-- 
cgit v1.2.3