diff options
| author | ppedrot | 2012-06-01 20:08:33 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 20:08:33 +0000 |
| commit | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (patch) | |
| tree | ec5246ac1cfc741dc30c33fe6551216dfdef6a54 /toplevel | |
| parent | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (diff) | |
More cleaning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 485b46aef3..314d712dc0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1250,7 +1250,7 @@ let vernac_print = function | PrintUniverses (b, None) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in - pp (Univ.pr_universes univ) + msg_info (Univ.pr_universes univ) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_info (Auto.pr_applicable_hint ()) @@ -1258,11 +1258,11 @@ let vernac_print = function | PrintRewriteHintDbName s -> msg_info (Autorewrite.print_rewrite_hintdb s) | PrintHintDb -> msg_info (Auto.pr_searchtable ()) | PrintScopes -> - pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) + msg_info (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) | PrintScope s -> - pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) + msg_info (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> - pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) + msg_info (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) | PrintAbout qid -> msg_info (print_about qid) | PrintImplicit qid -> msg_info (print_impargs qid) | PrintAssumptions (o,r) -> |