Getting rid of Pp.msgnl and Pp.message.

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

15 files changed, 114 insertions, 108 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index a8075294ec..3f9c158efe 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -163,7 +163,7 @@ let make_instance_ident gr =
 
 let new_instance_message ident typ def =
   Flags.if_verbose
-  msgnl (str"new instance"++spc()
+  msg_info (str"new instance"++spc()
 	 ++Nameops.pr_id ident++spc()++str":"++spc()
 	 ++pr_constr typ++spc()++str":="++spc()
 	 ++pr_constr def)
@@ -204,7 +204,7 @@ let declare_class_instance gr ctx params =
     (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
   Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
   new_instance_message ident typ def
-  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Errors.print e)
+  with e -> msg_info (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Errors.print e)
 
 let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
   match kind_of_term t with
diff --git a/toplevel/class.ml b/toplevel/class.ml
index ad2eb69b46..f0636f2379 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -299,9 +299,8 @@ let try_add_new_coercion_with_source ref stre ~source =
 
 let add_coercion_hook stre ref =
   try_add_new_coercion ref stre;
-  Flags.if_verbose message
-    (string_of_qualid (shortest_qualid_of_global Idset.empty ref)
-    ^ " is now a coercion")
+  Flags.if_verbose msg_info
+    (pr_global_env Idset.empty ref ++ str " is now a coercion")
 
 let add_subclass_hook stre ref =
   let cl = class_of_global ref in
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 02cf8ffe49..08cbe0640b 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -47,10 +47,10 @@ let load_rcfile() =
 			 " found. Skipping rcfile loading."))
 	*)
     with e ->
-      (msgnl (str"Load of rcfile failed.");
+      (msg_info (str"Load of rcfile failed.");
        raise e)
   else
-    Flags.if_verbose msgnl (str"Skipping rcfile loading.")
+    Flags.if_verbose msg_info (str"Skipping rcfile loading.")
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2bc4fa97c3..a60e74f16b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -309,9 +309,9 @@ let parse_args arglist =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  msgnl (Errors.print e); exit 1
+	  pperrnl (Errors.print e); exit 1
       end
-    | e -> begin msgnl (Errors.print e); exit 1 end
+    | e -> begin pperrnl (Errors.print e); exit 1 end
 
 let init arglist =
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
@@ -344,8 +344,8 @@ let init arglist =
       outputstate ()
     with e ->
       flush_all();
-      if not !batch_mode then message "Error during initialization:";
-      msgnl (Toplevel.print_toplevel_error e);
+      if not !batch_mode then pperrnl
+        (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e);
       exit 1
   end;
   if !batch_mode then
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 57b623712c..31f5d29943 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -125,13 +125,13 @@ let find_mutually_recursive_statements thms =
 	  assert (rest=[]);
           (* One occ. of common coind ccls and no common inductive hyps *)
 	  if common_same_indhyp <> [] then
-	    if_verbose msgnl (str "Assuming mutual coinductive statements.");
+	    if_verbose msg_info (str "Assuming mutual coinductive statements.");
 	  flush_all ();
           indccl, true, []
       | [], _::_ ->
 	  if same_indccl <> [] &&
 	     list_distinct (List.map pi1 (List.hd same_indccl)) then
-	    if_verbose msgnl (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
+	    if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
           let possible_guards = List.map (List.map pi3) inds_hyps in
 	  (* assume the largest indices as possible *)
 	  list_last common_same_indhyp, false, possible_guards
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fe7394e940..74b9ebe26b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -113,36 +113,44 @@ let add_tactic_notation (n,prods,e) =
 (**********************************************************************)
 (* Printing grammar entries                                           *)
 
-let print_grammar = function
+let entry_buf = Buffer.create 64
+
+let pr_entry e =
+  let () = Buffer.clear entry_buf in
+  let ft = Format.formatter_of_buffer entry_buf in
+  let () = Gram.entry_print ft e in
+  str (Buffer.contents entry_buf)
+
+let pr_grammar = function
   | "constr" | "operconstr" | "binder_constr" ->
-      msgnl (str "Entry constr is");
-      Gram.entry_print Pcoq.Constr.constr;
-      msgnl (str "and lconstr is");
-      Gram.entry_print Pcoq.Constr.lconstr;
-      msgnl (str "where binder_constr is");
-      Gram.entry_print Pcoq.Constr.binder_constr;
-      msgnl (str "and operconstr is");
-      Gram.entry_print Pcoq.Constr.operconstr;
+      str "Entry constr is" ++ fnl () ++
+      pr_entry Pcoq.Constr.constr ++
+      str "and lconstr is" ++ fnl () ++
+      pr_entry Pcoq.Constr.lconstr ++
+      str "where binder_constr is" ++ fnl () ++
+      pr_entry Pcoq.Constr.binder_constr ++
+      str "and operconstr is" ++ fnl () ++
+      pr_entry Pcoq.Constr.operconstr
   | "pattern" ->
-      Gram.entry_print Pcoq.Constr.pattern
+      pr_entry Pcoq.Constr.pattern
   | "tactic" ->
-      msgnl (str "Entry tactic_expr is");
-      Gram.entry_print Pcoq.Tactic.tactic_expr;
-      msgnl (str "Entry binder_tactic is");
-      Gram.entry_print Pcoq.Tactic.binder_tactic;
-      msgnl (str "Entry simple_tactic is");
-      Gram.entry_print Pcoq.Tactic.simple_tactic;
+      str "Entry tactic_expr is" ++ fnl () ++
+      pr_entry Pcoq.Tactic.tactic_expr ++
+      str "Entry binder_tactic is" ++ fnl () ++
+      pr_entry Pcoq.Tactic.binder_tactic ++
+      str "Entry simple_tactic is" ++ fnl () ++
+      pr_entry Pcoq.Tactic.simple_tactic
   | "vernac" ->
-      msgnl (str "Entry vernac is");
-      Gram.entry_print Pcoq.Vernac_.vernac;
-      msgnl (str "Entry command is");
-      Gram.entry_print Pcoq.Vernac_.command;
-      msgnl (str "Entry syntax is");
-      Gram.entry_print Pcoq.Vernac_.syntax;
-      msgnl (str "Entry gallina is");
-      Gram.entry_print Pcoq.Vernac_.gallina;
-      msgnl (str "Entry gallina_ext is");
-      Gram.entry_print Pcoq.Vernac_.gallina_ext;
+      str "Entry vernac is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.vernac ++
+      str "Entry command is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.command ++
+      str "Entry syntax is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.syntax ++
+      str "Entry gallina is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.gallina ++
+      str "Entry gallina_ext is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.gallina_ext
   | _ -> error "Unknown or unprintable grammar entry."
 
 (**********************************************************************)
@@ -594,7 +602,7 @@ let is_not_small_constr = function
 let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
-      message ("Identifier '"^k^"' now a keyword");
+      msg_info (str ("Identifier '"^k^"' now a keyword"));
       Lexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -603,7 +611,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      message ("Identifier '"^k^"' now a keyword");
+      msg_info (str ("Identifier '"^k^"' now a keyword"));
       Lexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -857,7 +865,7 @@ let find_precedence lev etyps symbols =
 	    error "The level of the leftmost non-terminal cannot be changed."
 	| ETName | ETBigint | ETReference ->
 	    if lev = None then
-	      ([msgnl,str "Setting notation at level 0."],0)
+	      ([msg_info,str "Setting notation at level 0."],0)
 	    else
 	    if lev <> Some 0 then
 	      error "A notation starting with an atomic expression must be at level 0."
@@ -877,7 +885,7 @@ let find_precedence lev etyps symbols =
       (match list_last symbols with Terminal _ -> true |_ -> false)
       ->
       if lev = None then
-	([msgnl,str "Setting notation at level 0."], 0)
+	([msg_info,str "Setting notation at level 0."], 0)
       else [],Option.get lev
   | _ ->
       if lev = None then error "Cannot determine the level.";
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index deed9d0359..f34b0ccaee 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -56,7 +56,7 @@ val add_syntactic_definition : identifier -> identifier list * constr_expr ->
 
 (** Print the Camlp4 state of a grammar *)
 
-val print_grammar : string -> unit
+val pr_grammar : string -> Pp.std_ppcmds
 
 val check_infix_modifiers : syntax_modifier list -> unit
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index e13b80dc7f..4f55cb896f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -299,10 +299,10 @@ let cache_ml_module_object (_,{mnames=mnames}) =
            let info = str"[Loading ML file " ++ str fname ++ str" ..." in
 	   try
              load_ml_object mname fname;
-             if_verbose msgnl (info ++ str" done]");
+             if_verbose msg_info (info ++ str" done]");
              add_loaded_module mname
            with e ->
-	     if_verbose msgnl (info ++ str" failed]");
+	     if_verbose msg_info (info ++ str" failed]");
 	     raise e
 	 else
 	      error ("Dynamic link not supported (module "^name^")")
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 5f07001ca9..aa6fbffe40 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -36,7 +36,7 @@ let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
 let trace s =
-  if !Flags.debug then (msgnl s; msgerr s)
+  if !Flags.debug then (msg_debug s; msgerr s)
   else ()
 
 let succfix (depth, fixrels) =
@@ -348,8 +348,7 @@ type program_info = {
   prg_hook : unit Tacexpr.declaration_hook;
 }
 
-let assumption_message id =
-  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
+let assumption_message = Declare.assumption_message
 
 let (set_default_tactic, get_default_tactic, print_default_tactic) = 
   Tactic_option.declare_tactic_option "Program tactic"
@@ -675,11 +674,11 @@ type progress =
 let obligations_message rem =
   if rem > 0 then
     if rem = 1 then
-      Flags.if_verbose msgnl (int rem ++ str " obligation remaining")
+      Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
     else
-      Flags.if_verbose msgnl (int rem ++ str " obligations remaining")
+      Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
   else
-    Flags.if_verbose msgnl (str "No more obligations remaining")
+    Flags.if_verbose msg_info (str "No more obligations remaining")
 
 let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
@@ -879,7 +878,7 @@ and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
 and auto_solve_obligations n ?oblset tac : progress =
-  Flags.if_verbose msgnl (str "Solving obligations automatically...");
+  Flags.if_verbose msg_info (str "Solving obligations automatically...");
   try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
 
 open Pp
@@ -887,13 +886,13 @@ let show_obligations_of_prg ?(msg=true) prg =
   let n = prg.prg_name in
   let obls, rem = prg.prg_obligations in
   let showed = ref 5 in
-    if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
+    if msg then msg_info (int rem ++ str " obligation(s) remaining: ");
     Array.iteri (fun i x ->
 		   match x.obl_body with
 		   | None ->
 		       if !showed > 0 then (
 			 decr showed;
-			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
 				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ 
 					    str "." ++ fnl ())))
@@ -911,7 +910,7 @@ let show_obligations ?(msg=true) n =
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
-    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
+    (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
 	     Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 8212afe290..26e9879740 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -109,7 +109,7 @@ val try_solve_obligations : Names.identifier option -> Proof_type.tactic option
 
 val show_obligations : ?msg:bool -> Names.identifier option -> unit
 
-val show_term : Names.identifier option -> unit
+val show_term : Names.identifier option -> std_ppcmds
 
 val admit_obligations : Names.identifier option -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d78a439908..a81dfa1351 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -210,7 +210,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                     const_entry_opaque = false } in
 		  let k = (DefinitionEntry cie,IsDefinition kind) in
 		  let kn = declare_constant ~internal:KernelSilent fid k in
-		  Flags.if_verbose message (string_of_id fid ^" is defined");
+		  Declare.definition_message fid;
 		  kn
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 952f80aad3..7991d0e582 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -355,7 +355,7 @@ let do_vernac () =
     try
       raw_do_vernac top_buffer.tokens
     with e ->
-      msgnl (print_toplevel_error (process_error e))
+      ppnl (print_toplevel_error (process_error e))
   end;
   flush_all()
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6d37e0d780..d6178cd624 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -159,9 +159,9 @@ let verbose_phrase verbch loc =
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        message s;
+        ppnl (str s);
         pp_flush()
-    | _ -> ()
+    | None -> ()
 
 exception End_of_input
 
@@ -194,7 +194,7 @@ let pr_new_syntax loc ocom =
   if !beautify_file then
     pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
-    msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
@@ -251,7 +251,7 @@ let rec vernac_com interpfun checknav (loc,com) =
 	  | e ->
 	      (* Anomalies are re-raised by the next line *)
 	      let msg = Errors.print_no_anomaly e in
-	      if_verbose msgnl
+	      if_verbose msg_info
 		(str "The command has indeed failed with message:" ++
 		 fnl () ++ str "=> " ++ hov 0 msg)
 	end
@@ -260,7 +260,7 @@ let rec vernac_com interpfun checknav (loc,com) =
 	  let tstart = System.get_time() in
           interp v;
 	  let tend = get_time() in
-          msgnl (str"Finished transaction in " ++
+          msg_info (str"Finished transaction in " ++
                    System.fmt_time_difference tstart tend)
 
     | VernacTimeout(n,v) ->
@@ -357,7 +357,7 @@ let compile verbosely f =
   if !Flags.xml_export then !xml_start_library ();
   let _ = load_vernac verbosely long_f_dot_v in
   if Pfedit.get_all_proof_names () <> [] then
-    (message "Error: There are pending proofs"; exit 1);
+    (pperrnl (str "Error: There are pending proofs"); exit 1);
   if !Flags.xml_export then !xml_end_library ();
   Dumpglob.end_dump_glob ();
   Library.save_library_to ldir (long_f_dot_v ^ "o")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index db3877dffc..282e2d051b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -71,7 +71,7 @@ let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
   let pprf = Proof.partial_proof p in
-  msgnl (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+  msg_info (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
 
 let show_node () =
   (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
@@ -81,10 +81,10 @@ let show_node () =
 let show_script () =
   let prf = Pfedit.get_current_proof_name () in
   let cmds = Backtrack.get_script prf in
-  msgnl (Pp.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
+  msg_info (Pp.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
 
 let show_thesis () =
-     msgnl (anomaly "TODO" )
+     msg_info (anomaly "TODO" )
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -118,12 +118,12 @@ let show_intro all =
   if all
   then
     let lid = Tactics.find_intro_names l gl in
-    msgnl (hov 0 (prlist_with_sep  spc pr_id lid))
+    msg_info (hov 0 (prlist_with_sep  spc pr_id lid))
   else
     try
       let n = list_last l in
-      msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
-    with Failure "list_last" -> message ""
+      msg_info (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+    with Failure "list_last" -> ()
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -176,7 +176,7 @@ let print_loadpath dir =
   let l = match dir with
     | None -> l
     | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
-  msgnl (Pp.t (str "Logical Path:                 " ++
+  msg_info (Pp.t (str "Logical Path:                 " ++
 		 tab () ++ str "Physical path:" ++ fnl () ++
 		 prlist_with_sep fnl print_path_entry l))
 
@@ -199,23 +199,23 @@ let print_module r =
     let globdir = Nametab.locate_dir qid in
       match globdir with
 	  DirModule (dirpath,(mp,_)) ->
-	    msgnl (Printmod.print_module (Printmod.printable_body dirpath) mp)
+	    msg_info (Printmod.print_module (Printmod.printable_body dirpath) mp)
 	| _ -> raise Not_found
   with
-      Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid)
+      Not_found -> msg_info (str"Unknown Module " ++ pr_qualid qid)
 
 let print_modtype r =
   let (loc,qid) = qualid_of_reference r in
   try
     let kn = Nametab.locate_modtype qid in
-    msgnl (Printmod.print_modtype kn)
+    msg_info (Printmod.print_modtype kn)
   with Not_found ->
     (* Is there a module of this name ? If yes we display its type *)
     try
       let mp = Nametab.locate_module qid in
-      msgnl (Printmod.print_module false mp)
+      msg_info (Printmod.print_module false mp)
     with Not_found ->
-      msgnl (str"Unknown Module Type or Module " ++ pr_qualid qid)
+      msg_info (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let dump_universes_gen g s =
   let output = open_out s in
@@ -249,7 +249,7 @@ let dump_universes_gen g s =
   try
     Univ.dump_universes output_constraint g;
     close ();
-    msgnl (str ("Universes written to file \""^s^"\"."))
+    msg_info (str ("Universes written to file \""^s^"\"."))
   with
       e -> close (); raise e
 
@@ -263,15 +263,15 @@ let dump_universes sorted s =
 
 let locate_file f =
   let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
-  msgnl (str file)
+  msg_info (str file)
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->
-      msgnl (hov 0
+      msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
 	 str file))
   | Library.LibInPath, fulldir, file ->
-      msgnl (hov 0
+      msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 let msg_notfound_library loc qid = function
   | Library.LibUnmappedDir ->
@@ -280,7 +280,7 @@ let msg_notfound_library loc qid = function
         strbrk "Cannot find a physical path bound to logical path " ++
            pr_dirpath dir ++ str".")
   | Library.LibNotFound ->
-      msgnl (hov 0
+      msg_info (hov 0
 	(strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
   | e -> assert false
 
@@ -300,11 +300,11 @@ let print_located_module r =
 	str "No module is referred to by basename "
       else
 	str "No module is referred to by name ") ++ pr_qualid qid
-  in msgnl msg
+  in msg_info msg
 
 let print_located_tactic r =
   let (loc,qid) = qualid_of_reference r in
-  msgnl
+  msg_info
     (try
       str "Ltac " ++
       pr_path (Nametab.path_of_tactic (Nametab.locate_tactic qid))
@@ -494,7 +494,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
     id binders_ast (Enforce mty_ast) []
   in
     Dumpglob.dump_moddef loc mp "mod";
-    if_verbose message ("Module "^ string_of_id id ^" is declared");
+    if_verbose msg_info (str ("Module "^ string_of_id id ^" is declared"));
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -514,8 +514,8 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 	 id binders_ast mty_ast_o
        in
 	 Dumpglob.dump_moddef loc mp "mod";
-	 if_verbose message
-	   ("Interactive Module "^ string_of_id id ^" started") ;
+	 if_verbose msg_info
+	   (str ("Interactive Module "^ string_of_id id ^" started"));
          List.iter
            (fun (export,id) ->
              Option.iter
@@ -535,15 +535,15 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 	  id binders_ast mty_ast_o mexpr_ast_l
        in
 	 Dumpglob.dump_moddef loc mp "mod";
-	 if_verbose message
-	   ("Module "^ string_of_id id ^" is defined");
+	 if_verbose msg_info
+	   (str ("Module "^ string_of_id id ^" is defined"));
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
            export
 
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+  if_verbose msg_info (str ("Module "^ string_of_id id ^" is defined"));
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -562,8 +562,8 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
        let mp = Declaremods.start_modtype
 	 Modintern.interp_modtype id binders_ast mty_sign in
         Dumpglob.dump_moddef loc mp "modtype";
-	if_verbose message
-	  ("Interactive Module Type "^ string_of_id id ^" started");
+	if_verbose msg_info
+	  (str ("Interactive Module Type "^ string_of_id id ^" started"));
         List.iter
          (fun (export,id) ->
            Option.iter
@@ -582,13 +582,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
           Modintern.interp_modexpr_or_modtype
 	  id binders_ast mty_sign mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
-	  if_verbose message
-	    ("Module Type "^ string_of_id id ^" is defined")
+	  if_verbose msg_info
+	    (str ("Module Type "^ string_of_id id ^" is defined"))
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose message ("Module Type "^ string_of_id id ^" is defined")
+  if_verbose msg_info (str ("Module Type "^ string_of_id id ^" is defined"))
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_modexpr_or_modtype l
@@ -637,7 +637,7 @@ let vernac_coercion stre ref qids qidt =
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
   Class.try_add_new_coercion_with_target ref' stre ~source ~target;
-  if_verbose msgnl (pr_global ref' ++ str " is now a coercion")
+  if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion stre id qids qidt =
   let target = cl_of_qualid qidt in
@@ -734,13 +734,13 @@ let vernac_declare_ml_module local l =
 				    l)
 
 let vernac_chdir = function
-  | None -> message (Sys.getcwd())
+  | None -> msg_info (str (Sys.getcwd()))
   | Some path ->
       begin
 	try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
 	with Sys_error err -> msg_warning (str ("Cd failed: " ^ err))
       end;
-      if_verbose message (Sys.getcwd())
+      if_verbose msg_info (str (Sys.getcwd()))
 
 
 (********************)
@@ -1228,7 +1228,7 @@ let vernac_print = function
   | PrintFullContext-> msg_info (print_full_context_typ ())
   | PrintSectionContext qid -> msg_info (print_sec_context_typ qid)
   | PrintInspect n -> msg_info (inspect n)
-  | PrintGrammar ent -> Metasyntax.print_grammar ent
+  | PrintGrammar ent -> msg_info (Metasyntax.pr_grammar ent)
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> msg_info (print_modules ())
   | PrintModule qid -> print_module qid
@@ -1320,9 +1320,9 @@ let vernac_search s r =
       msg_info (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)
 
 let vernac_locate = function
-  | LocateTerm (AN qid) -> msgnl (print_located_qualid qid)
+  | LocateTerm (AN qid) -> msg_info (print_located_qualid qid)
   | LocateTerm (ByNotation (_,ntn,sc)) ->
-      ppnl
+      msg_info
         (Notation.locate_notation
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
@@ -1374,20 +1374,20 @@ let vernac_abort = function
   | None ->
       Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
       delete_current_proof ();
-      if_verbose message "Current goal aborted";
+      if_verbose msg_info (str "Current goal aborted");
       if !pcoq <> None then (Option.get !pcoq).abort ""
   | Some id ->
       Backtrack.mark_unreachable [snd id];
       delete_proof id;
       let s = string_of_id (snd id) in
-      if_verbose message ("Goal "^s^" aborted");
+      if_verbose msg_info (str ("Goal "^s^" aborted"));
       if !pcoq <> None then (Option.get !pcoq).abort s
 
 let vernac_abort_all () =
   if refining() then begin
     Backtrack.mark_unreachable (Pfedit.get_all_proof_names ());
     delete_all_proofs ();
-    message "Current goals aborted"
+    msg_info (str "Current goals aborted")
   end else
     error "No proof-editing in progress."
 
@@ -1471,7 +1471,7 @@ let vernac_show = function
   | ShowExistentials -> show_top_evars ()
   | ShowTree -> show_prooftree ()
   | ShowProofNames ->
-      msgnl (pr_sequence pr_id (Pfedit.get_all_proof_names()))
+      msg_info (pr_sequence pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
   | ShowThesis -> show_thesis ()
@@ -1489,7 +1489,7 @@ let vernac_check_guard () =
     with UserError(_,s) ->
       (str ("Condition violated: ") ++s)
   in
-  msgnl message
+  msg_info message
 
 let interp c = match c with
   (* Control (done in vernac) *)
@@ -1590,7 +1590,7 @@ let interp c = match c with
   | VernacPrint p -> vernac_print p
   | VernacSearch (s,r) -> vernac_search s r
   | VernacLocate l -> vernac_locate l
-  | VernacComments l -> if_verbose message ("Comments ok\n")
+  | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
   | VernacNop -> ()
 
   (* Proof management *)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 4862419e24..65c74ae0ba 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -62,5 +62,5 @@ let call (opn,converted_args) =
     | Drop -> raise Drop
     | e ->
         if !Flags.debug then
-	  msgnl (str"Vernac Interpreter " ++ str !loc);
+	  msg_debug (str"Vernac Interpreter " ++ str !loc);
         raise e