From ee6526fa035ea31f4219a773a4f38516d0f3c989 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 3 Oct 2010 13:11:46 +0000 Subject: Making display of various informations about constants more modular: - use list of non-newline-ended phrases instead of newline-separated texts because newline-separated texts does not support well being put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()'' prints "b" at indentation 2 while to get the expected output, one would have needed to have the fnl outside the box as in ''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()'' - also reason over lists of explicitly non-empty lines instead of checking for "mt" lines to skip The reason of this is to permit nesting of printing infos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/vernacentries.ml') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f6fb8aa51..a0404e18c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1090,7 +1090,7 @@ let vernac_print = function pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) - | PrintAbout qid -> msgnl (print_about qid) + | PrintAbout qid -> msg (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) | PrintAssumptions (o,r) -> -- cgit v1.2.3