Cleaning Pp.ppnl use

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 21 insertions, 22 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 12ce73a5b0..2f5ed1181b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -380,7 +380,7 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
 			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 		       constrimpls)
       impls;
-  if_verbose ppnl (minductive_message names);
+  if_verbose msg_info (minductive_message names);
   declare_default_schemes mind;
   mind
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4f55cb896f..176c0577ee 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -324,11 +324,11 @@ let declare_ml_modules local l =
 
 let print_ml_path () =
   let l = !coq_mlpath_copy in
-  ppnl (str"ML Load Path:" ++ fnl () ++ str"  " ++
-          hv 0 (prlist_with_sep fnl str l))
+  str"ML Load Path:" ++ fnl () ++ str"  " ++
+          hv 0 (prlist_with_sep fnl str l)
 
 	  (* Printing of loaded ML modules *)
 
 let print_ml_modules () =
   let l = get_loaded_modules () in
-  pp (str"Loaded ML Modules: " ++ pr_vertical_list str l)
+  str"Loaded ML Modules: " ++ pr_vertical_list str l
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 99b96ed7bd..66fbbbded1 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -74,6 +74,5 @@ type ml_module_object = {
 
 val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
-val print_ml_path : unit -> unit
-
-val print_ml_modules : unit -> unit
+val print_ml_path : unit -> Pp.std_ppcmds
+val print_ml_modules : unit -> Pp.std_ppcmds
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa6fbffe40..1b420407ca 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -916,16 +916,16 @@ let show_term n =
 
 let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
-  Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+  let info = str (string_of_id n) ++ str " has type-checked" in
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
-    Flags.if_verbose ppnl (str ".");
+    Flags.if_verbose msg_info (info ++ str ".");
     let cst = declare_definition prg in
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
       progmap_add n prg;
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index a81dfa1351..f9a3d2c122 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -123,7 +123,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then errorlabstrm "structure" st;
-  Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
+  Flags.if_verbose msg_warning (hov 0 (str"Warning: " ++ st))
 
 type field_status =
   | NoProjection of name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 282e2d051b..485b46aef3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1233,20 +1233,20 @@ let vernac_print = function
   | PrintModules -> msg_info (print_modules ())
   | PrintModule qid -> print_module qid
   | PrintModuleType qid -> print_modtype qid
-  | PrintMLLoadPath -> Mltop.print_ml_path ()
-  | PrintMLModules -> Mltop.print_ml_modules ()
+  | PrintMLLoadPath -> msg_info (Mltop.print_ml_path ())
+  | PrintMLModules -> msg_info (Mltop.print_ml_modules ())
   | PrintName qid ->
       if !pcoq <> None then (Option.get !pcoq).print_name qid
       else msg_info (print_name qid)
-  | PrintGraph -> ppnl (Prettyp.print_graph())
-  | PrintClasses -> ppnl (Prettyp.print_classes())
-  | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
-  | PrintInstances c -> ppnl (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
-  | PrintCoercions -> ppnl (Prettyp.print_coercions())
+  | PrintGraph -> msg_info (Prettyp.print_graph())
+  | PrintClasses -> msg_info (Prettyp.print_classes())
+  | PrintTypeClasses -> msg_info (Prettyp.print_typeclasses())
+  | PrintInstances c -> msg_info (Prettyp.print_instances (smart_global c))
+  | PrintLtac qid -> msg_info (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
+  | PrintCoercions -> msg_info (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
-      ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
-  | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
+      msg_info (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+  | PrintCanonicalConversions -> msg_info (Prettyp.print_canonical_projections ())
   | PrintUniverses (b, None) ->
     let univ = Global.universes () in
     let univ = if b then Univ.sort_universes univ else univ in
@@ -1255,7 +1255,7 @@ let vernac_print = function
   | PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_info (Auto.pr_applicable_hint ())
   | PrintHintDbName s -> msg_info (Auto.pr_hint_db_by_name s)
-  | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
+  | 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))