diff options
| author | aspiwack | 2007-05-11 17:00:58 +0000 |
|---|---|---|
| committer | aspiwack | 2007-05-11 17:00:58 +0000 |
| commit | 2dbe106c09b60690b87e31e58d505b1f4e05b57f (patch) | |
| tree | 4476a715b796769856e67f6eb5bb6eb60ce6fb57 /parsing/ppvernac.ml | |
| parent | 95f043a4aa63630de133e667f3da1f48a8f9c4f3 (diff) | |
Processor integers + Print assumption (see coqdev mailing list for the
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7ccd8dd65d..62af97b439 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -814,12 +814,15 @@ let rec pr_vernac = function | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n - | PrintSetoids -> str"Print Setoids" + | PrintSetoids -> str"Print Setoids" | PrintScopes -> str"Print Scopes" | PrintScope s -> str"Print Scope" ++ spc() ++ str s | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s | PrintAbout qid -> str"About" ++ spc() ++ pr_reference qid | 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 in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr | VernacLocate loc -> |