diff options
| author | aspiwack | 2007-05-30 17:31:50 +0000 |
|---|---|---|
| committer | aspiwack | 2007-05-30 17:31:50 +0000 |
| commit | fb7465c9c4d3e88cb6b4c388901db25d3ae923b8 (patch) | |
| tree | cdc449984a4e7f102e7b37cb2efd8f7bde2088a6 /parsing | |
| parent | 7350f5de205ea54e277be1d82cc045788182f82e (diff) | |
Corrections dans le Print Assumption. Les definitions locales ("Let")
sont maintenant prises en compte (ca a l'air de marcher). En plus j'ai
corrige l'ordre d'impression pour que ca imprime les noms dans l'ordre
alphabetique (avant c'etait l'ordre inverse, etonnament perturbant).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9873 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | parsing/printer.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f12f730610..668cfe6f30 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -828,7 +828,7 @@ let rec pr_vernac = function | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid (* spiwack: command printing all the axioms and section variables used in a term *) - | PrintNeededAssumptions qid -> str"Print Needed Assumptions"++spc()++pr_reference qid + | PrintNeededAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr | VernacLocate loc -> diff --git a/parsing/printer.ml b/parsing/printer.ml index 307e0af231..97c1f6b7bf 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -486,7 +486,7 @@ let pr_assumptionset env s = str "Section Variables:" ++ fnl () ++ (Environ.AssumptionSet.fold (function Variable (id,typ ) -> fun s -> - str (string_of_identifier id)++str " : "++pr_ltype typ++spc ()++s) + s++str (string_of_identifier id)++str " : "++pr_ltype typ++spc ()) vars (fnl ())) else mt () @@ -494,7 +494,7 @@ let pr_assumptionset env s = if not (Environ.AssumptionSet.is_empty axioms) then str "Axioms:" ++ fnl () ++ (Environ.AssumptionSet.fold - (function Axiom (cst, typ) -> fun s -> (pr_constant env cst)++str " : "++pr_ltype typ++spc ()++s) + (function Axiom (cst, typ) -> fun s -> s++(pr_constant env cst)++str " : "++pr_ltype typ++spc ()) axioms (mt ())) else mt () |