diff options
| author | herbelin | 2011-06-21 18:43:33 +0000 |
|---|---|---|
| committer | herbelin | 2011-06-21 18:43:33 +0000 |
| commit | 6810929f652be3ebe40de86fe360665c6aded049 (patch) | |
| tree | 2e1a337d99c206f98837cab110f4d3f39ec8566e /proofs | |
| parent | 580539fce36067d7c6ee89cbcb8707fd29ebc117 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 3 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
4 files changed, 6 insertions, 5 deletions
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)) |