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

53 files changed, 260 insertions, 255 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 5b8507304b..976120ffec 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -99,11 +99,11 @@ let check_one_lib admit (dir,m) =
      also check if it carries a validation certificate (yet to
      be implemented). *)
   if LibrarySet.mem dir admit then
-    (Flags.if_verbose msgnl
+    (Flags.if_verbose ppnl
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md dig)
   else
-    (Flags.if_verbose msgnl
+    (Flags.if_verbose ppnl
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md dig);
   Flags.if_verbose pp (fnl());
@@ -159,7 +159,7 @@ let remove_load_path dir =
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
     match list_filter2 (fun p d -> p = phys_path) !load_paths with
@@ -299,9 +299,9 @@ let intern_from_file (dir, f) =
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
           (name_clash_message dir md.md_name f);
-      Flags.if_verbose msgnl(str" done]");
+      Flags.if_verbose ppnl (str" done]");
       md,table,digest
-    with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
   mk_library md f table digest
 
@@ -360,11 +360,11 @@ let recheck_library ~norec ~admit ~check =
   let nochk =
     List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
   (* *)
-  Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib nochk) needed;
-  Flags.if_verbose msgnl(str"Modules were successfully checked")
+  Flags.if_verbose ppnl (str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index cdb0ade744..1cc47fde32 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -55,12 +55,12 @@ let print_context env =
          env_modules=mods; env_modtypes=mtys};
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
-    msgnl(hov 0
+    ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
-      fnl()))
+      fnl())); pp_flush()
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 7ea55d833c..848fd22f4e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -292,7 +292,7 @@ let parse_args argv =
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
-	(msgnl (str ("Directory '"^s^"' does not exist")); exit 1);
+	(pperrnl (str ("Directory '"^s^"' does not exist")); exit 1);
       Flags.coqlib := s;
       Flags.coqlib_spec := true;
       parse rem
@@ -332,7 +332,7 @@ let parse_args argv =
         Flags.make_silent true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
-        msgnl (str "Unknown option " ++ str s); exit 1
+        pperrnl (str "Unknown option " ++ str s); exit 1
     | s :: rem ->  add_compile s; parse rem
   in
   try
@@ -342,9 +342,9 @@ let parse_args argv =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  msgnl (explain_exn e); exit 1
+	  pperrnl (explain_exn e); exit 1
       end
-    | e -> begin msgnl (explain_exn e); exit 1 end
+    | e -> begin pperrnl (explain_exn e); exit 1 end
 
 
 (* To prevent from doing the initialization twice *)
@@ -361,8 +361,7 @@ let init_with_argv argv =
       engage ();
     with e ->
       flush_all();
-      message "Error during initialization :";
-      msgnl (explain_exn e);
+      pperrnl (str "Error during initialization :" ++ (explain_exn e));
       exit 1
   end
 
diff --git a/checker/closure.ml b/checker/closure.ml
index 069b820176..c30b305575 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -29,7 +29,7 @@ let reset () =
   beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
 
 let stop() =
-  msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
          str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index c12c54cfd9..a8f151e7e2 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -526,7 +526,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose msgnl (str "  checking ind: " ++ pr_mind kn);
+  Flags.if_verbose ppnl (str "  checking ind: " ++ pr_mind kn); pp_flush ();
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints mib.mind_constraints env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7a66ced77b..a51b66ce0e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose msgnl (str "  checking cst: " ++ prcon kn);
+  Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
 (*  let env = add_constraints cb.const_constraints env in*)
   let env' = check_named_ctxt env cb.const_hyps in
   (match cb.const_type with
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 57a9011cfd..7fe37e29d5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -182,7 +182,7 @@ let stamp_library file digest = ()
    warning is issued in case of mismatch *)
 let import file (dp,mb,depends,engmt as vo) digest =
   Validate.apply !Flags.debug val_vo vo;
-  Flags.if_verbose msgnl (str "*** vo structure validated ***");
+  Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush ();
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
diff --git a/kernel/closure.ml b/kernel/closure.ml
index d62ac79bfe..0518ab2491 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -44,7 +44,7 @@ let reset () =
   prune := 0
 
 let stop() =
-  msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
          str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
 
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 8d8483b49f..9f54512a1f 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -109,7 +109,7 @@ module type GrammarSig = sig
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> parsable -> 'a
-  val entry_print : 'a entry -> unit
+  val entry_print : Format.formatter -> 'a entry -> unit
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
@@ -129,9 +129,9 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let entry_create = Entry.create
   let entry_parse = Entry.parse
 IFDEF CAMLP5_6_02_1 THEN
-  let entry_print x = Entry.print !Pp_control.std_ft x
+  let entry_print ft x = Entry.print ft x
 ELSE
-  let entry_print = Entry.print
+  let entry_print _ x = Entry.print x
 END
   let srules' = Gramext.srules
   let parse_tokens_after_filter = Entry.parse_token
@@ -149,7 +149,7 @@ module type GrammarSig = sig
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> parsable -> 'a
-  val entry_print : 'a entry -> unit
+  val entry_print : Format.formatter -> 'a entry -> unit
   val srules' : production_rule list -> symbol
 end
 
@@ -162,7 +162,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   let action = Action.mk
   let entry_create = Entry.mk
   let entry_parse e s = parse e (*FIXME*)Loc.ghost s
-  let entry_print x = Entry.print !Pp_control.std_ft x
+  let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 135343092d..8b3f6ff244 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -103,7 +103,6 @@ val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
-val message : string -> unit       (** = pPNL *)
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
@@ -122,6 +121,7 @@ val msg : std_ppcmds -> unit
 val msgnl : std_ppcmds -> unit
 val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
+val message : string -> unit       (** = pPNL *)
 
 (** {6 Location management. } *)
 
diff --git a/lib/system.ml b/lib/system.ml
index 1537f48927..238efcff75 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -105,8 +105,8 @@ let open_trapping_failure name =
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str filename ++ str" which is corrupted!" )
+  with _ -> msg_warning
+    (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in ch =
diff --git a/library/declare.ml b/library/declare.ml
index c386ac6aa8..b0c1f0cc54 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -282,7 +282,7 @@ let declare_mind isrecord mie =
 let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
-  Flags.if_verbose msgnl (match l with
+  Flags.if_verbose msg_info (match l with
   | [] -> anomaly "no recursive definition"
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
@@ -297,7 +297,7 @@ let fixpoint_message indexes l =
 		    | None -> mt ()))
 
 let cofixpoint_message l =
-  Flags.if_verbose msgnl (match l with
+  Flags.if_verbose msg_info (match l with
   | [] -> anomaly "No corecursive definition."
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -307,7 +307,7 @@ let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose msgnl (pr_id id ++ str " is defined")
+  Flags.if_verbose msg_info (pr_id id ++ str " is defined")
 
 let assumption_message id =
-  Flags.if_verbose msgnl (pr_id id ++ str " is assumed")
+  Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index d4229ff0b0..7d7f2b10d3 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -126,7 +126,7 @@ open Pp
 
 VERNAC COMMAND EXTEND Show_Solver
 | [ "Show" "Obligation" "Tactic" ] -> [
-    msgnl (str"Program obligation tactic is " ++ print_default_tactic ()) ]
+    msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
 END
 
 VERNAC COMMAND EXTEND Show_Obligations
@@ -135,8 +135,8 @@ VERNAC COMMAND EXTEND Show_Obligations
 END
 
 VERNAC COMMAND EXTEND Show_Preterm
-| [ "Preterm" "of" ident(name) ] -> [ show_term (Some name) ]
-| [ "Preterm" ] -> [ show_term None ]
+| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ]
+| [ "Preterm" ] -> [ msg_info (show_term None) ]
 END
 
 open Pp
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 699f1f3dfd..6fda2284a8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -23,8 +23,8 @@ let init_size=5
 
 let cc_verbose=ref false
 
-let debug f x =
-  if !cc_verbose then f x
+let debug x =
+  if !cc_verbose then msg_debug x
 
 let _=
   let gdopt=
@@ -512,7 +512,7 @@ let add_inst state (inst,int_subst) =
   check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug msgnl (str "discarding redundant (dis)equality")
+    debug (str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -527,20 +527,18 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -566,8 +564,8 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
-		 str " and " ++ pr_idx_term state i2 ++ str ".")) ();
+  debug (str "Linking " ++ pr_idx_term state i1 ++
+		 str " and " ++ pr_idx_term state i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
@@ -606,9 +604,9 @@ let union state i1 i2 eq=
 	| _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug (fun () -> msgnl
+  debug
     (str "Merging " ++ pr_idx_term state eq.lhs ++
-       str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
+       str " and " ++ pr_idx_term state eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
@@ -619,8 +617,8 @@ let merge eq state = (* merge and no-merge *)
 	union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug (fun () -> msgnl
-    (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Updating term " ++ pr_idx_term state t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -680,8 +678,8 @@ let process_constructor_mark t i rep pac state =
 	    end
 
 let process_mark t m state =
-  debug (fun () -> msgnl
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -701,9 +699,9 @@ let check_disequalities state =
           if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
           else (str "No", check_aux q)
         in
-        let _ = debug (fun () -> msg_debug
+        let _ = debug
         (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-         pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+         pr_idx_term state dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
   in
@@ -889,7 +887,7 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug msgnl (str "Running E-matching algorithm ... ");
+    debug (str "Running E-matching algorithm ... ");
     try
       while true do
 	check_for_interrupt ();
@@ -900,7 +898,7 @@ let find_instances state =
     !res
 
 let rec execute first_run state =
-  debug msgnl (str "Executing ... ");
+  debug (str "Executing ... ");
   try
     while
       check_for_interrupt ();
@@ -910,7 +908,7 @@ let rec execute first_run state =
 	None ->
 	  if not(Intset.is_empty state.pa_classes) then
 	    begin
-	      debug msgnl (str "First run was incomplete, completing ... ");
+	      debug (str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -925,12 +923,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug msgnl (str "Out of instances ... ");
+		debug (str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug msgnl (str "Out of depth ... ");
+		debug (str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 78dbee3fe8..2d017f5cfe 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -71,7 +71,7 @@ module Termhash : Hashtbl.S with type key = term
 
 val constr_of_term : term -> constr
 
-val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
+val debug : Pp.std_ppcmds -> unit
 
 val forest : state -> forest
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7940009c6e..204af93d56 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -378,16 +378,16 @@ let build_term_to_complete uf meta pac =
 
 let cc_tactic depth additionnal_terms gls=
   Coqlib.check_required_library ["Coq";"Init";"Logic"];
-  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
+  let _ = debug (Pp.str "Reading subgoal ...") in
   let state = make_prb gls depth additionnal_terms in
-  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
+  let _ = debug (Pp.str "Problem built, solving ...") in
   let sol = execute true state in
-  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
+  let _ = debug (Pp.str "Computation completed.") in
   let uf=forest state in
     match sol with
 	None -> tclFAIL 0 (str "congruence failed") gls
       | Some reason ->
-	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
+	  debug (Pp.str "Goal solved, generating proof ...");
 	  match reason with
 	      Discrimination (i,ipac,j,jpac) ->
 		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
@@ -400,10 +400,10 @@ let cc_tactic depth additionnal_terms gls=
 		  List.map
 		    (build_term_to_complete uf newmeta)
 		    (epsilons uf) in
-		  Pp.msgnl
+		  Pp.msg_info
 		    (Pp.str "Goal is solvable by congruence but \
  some arguments are missing.");
-		  Pp.msgnl
+		  Pp.msg_info
 		    (Pp.str "  Try " ++
 		     hov 8
 		       begin
@@ -413,9 +413,8 @@ let cc_tactic depth additionnal_terms gls=
 			   (Termops.print_constr_env (pf_env gls))
 			   terms_to_complete ++
 			 str ")\","
-		       end);
-		  Pp.msgnl
-		    (Pp.str "  replacing metavariables by arbitrary terms.");
+		       end ++
+		    Pp.str "  replacing metavariables by arbitrary terms.");
 		  tclFAIL 0 (str "Incomplete") gls
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2c845ce324..f107007363 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -420,8 +420,9 @@ let print_one_decl struc mp decl =
   ignore (d.pp_struct struc);
   set_phase Impl;
   push_visible mp [];
-  msgnl (d.pp_decl decl);
-  pop_visible ()
+  let ans = d.pp_decl decl in
+  pop_visible ();
+  ans
 
 (*s Extraction of a ml struct to a file. *)
 
@@ -496,7 +497,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
   if Buffer.length buf <> 0 then begin
-    Pp.message (Buffer.contents buf);
+    Pp.msg_info (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -580,9 +581,13 @@ let simple_extraction r = match locate_ref [r] with
       let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
       warns ();
-      if is_custom r then msgnl (str "(** User defined extraction *)");
-      print_one_decl struc (modpath_of_r r) d;
-      reset ()
+      let flag =
+        if is_custom r then str "(** User defined extraction *)" ++ fnl()
+        else mt ()
+      in
+      let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
+      reset ();
+      Pp.msg_info ans
   | _ -> assert false
 
 
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index c846d2d0f3..a1c9898f2b 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -25,4 +25,4 @@ val mono_environment :
 (* Used by the Relation Extraction plugin *)
 
 val print_one_decl :
-  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit
+  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index fe86e1ae12..aa1e36f67a 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -121,7 +121,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionBlacklist
 | [ "Print" "Extraction" "Blacklist" ]
-  -> [ print_extraction_blacklist () ]
+  -> [ msg_info (print_extraction_blacklist ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionBlacklist
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 0efdbbb6b5..62ce89896a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -430,8 +430,8 @@ let check_loaded_modfile mp = match base_mp mp with
   | _ -> ()
 
 let info_file f =
-  Flags.if_verbose message
-    ("The file "^f^" has been created by extraction.")
+  Flags.if_verbose msg_info
+    (str ("The file "^f^" has been created by extraction."))
 
 
 (*S The Extraction auxiliary commands *)
@@ -738,8 +738,7 @@ let extraction_blacklist l =
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  msgnl
-    (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))
+  prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)
 
 (* Reset part *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 978760e8e9..185aa03ee2 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -192,7 +192,7 @@ val extraction_implicit : reference -> int_or_id list -> unit
 
 val extraction_blacklist : identifier list -> unit
 val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> unit
+val print_extraction_blacklist : unit -> Pp.std_ppcmds
 
 
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b6a0ef4c33..b009107dce 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -65,7 +65,7 @@ END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver
 | [ "Print" "Firstorder" "Solver" ] -> [
-    Pp.msgnl
+    Pp.msg_info
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
 END
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 467080531b..3aa57578d1 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -33,7 +33,7 @@ let ground_tac solver startseq gl=
   update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Pp.msgnl (Printer.pr_goal gl);
+    then Pp.msg_debug (Printer.pr_goal gl);
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 269439a535..1d48ef45b8 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -241,7 +241,7 @@ let print_cmap map=
       Ppconstr.pr_constr_expr xc ++
       cut () ++
       s in
-    msgnl (v 0
+    (v 0
 	     (str "-----" ++
 	      cut () ++
 	      CM.fold print_entry map (mt ()) ++
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 9f13e54cf0..e7d05d5a94 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -60,4 +60,4 @@ val extend_with_ref_list : global_reference list ->
 val extend_with_auto_hints : Auto.hint_db_name list ->
   t -> Proof_type.goal sigma -> t
 
-val print_cmap: global_reference list CM.t -> unit
+val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 046b65ee8f..bd5fd9c09c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -18,7 +18,7 @@ open Libnames
 open Globnames
 open Misctypes
 
-let msgnl = Pp.msgnl
+(* let msgnl = Pp.msgnl *)
 
 (*
 let observe strm =
@@ -60,17 +60,17 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
       else
 	begin
-	  Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
 	end;
       print_debug_queue false e;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 let do_observe_tac s tac g = 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 21f77e438d..42e5c36a8c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -36,7 +36,7 @@ let pr_elim_scheme el =
 
 let observe s =
   if do_observe ()
-  then Pp.msgnl s
+  then Pp.msg_debug s
 
 
 let pr_elim_scheme el =
@@ -54,7 +54,7 @@ let pr_elim_scheme el =
 
 let observe s =
   if do_observe ()
-  then Pp.msgnl s
+  then Pp.msg_debug s
 
 (*
    Transform an inductive induction principle into
@@ -394,9 +394,7 @@ let generate_functional_principle
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme)
 	    )
 	);
-	Flags.if_verbose
-	  (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined"))
-	  name;
+	Declare.definition_message name;
 	names := name :: !names
       in
       register_with_sort InProp;
@@ -676,8 +674,7 @@ let build_scheme fas =
 	 (Declare.declare_constant
 	    princ_id
 	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-       Flags.if_verbose
-	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
+       Declare.definition_message princ_id
     )
     fas
     bodies_types;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a169c28260..7b341e581b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -14,7 +14,7 @@ open Misctypes
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 (*let observennl strm =
   if do_observe ()
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 026b9ad0ec..8443959b4b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -153,9 +153,8 @@ open Declarations
 open Entries
 open Decl_kinds
 open Declare
-let definition_message id =
-  Flags.if_verbose message ((string_of_id id) ^ " is defined")
 
+let definition_message = Declare.definition_message
 
 let save with_clean id const (locality,kind) hook =
   let {const_entry_body = pft;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b463b6c27b..7745996c58 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -48,11 +48,11 @@ let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
   pr_with_bindings prc prc  (c,bl)
 
 (* The local debuging mechanism *)
-let msgnl = Pp.msgnl
+(* let msgnl = Pp.msgnl *)
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 (*let observennl strm =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5fcd495ef9..7cf438e6f5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -235,17 +235,17 @@ let rec print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+	Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
       else
 	begin
-	  Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+	  Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal);
 	end;
       print_debug_queue false e;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
+  then Pp.msg_debug strm
   else ()
 
 
@@ -413,7 +413,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    (fun g' -> 
 	      let ty_teq = pf_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
-		let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g' ++ fnl () ++ pr_id heq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+		let _,args = try destApp ty_teq with _ -> assert false in
 		args.(1),args.(2)
 	      in
 	      let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index a1ab6cd301..46d561ed85 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -533,7 +533,7 @@ let pp_info () =
 	int s_info.created_branches ++ str " created" ++ fnl () ++
 	str "Hypotheses : " ++
 	int s_info.created_hyps ++ str " created" ++ fnl () in
-    msgnl
+    msg_info
       ( str "Proof-search statistics :" ++ fnl () ++
 	count_info ++
 	str "Branch ends: " ++
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 60ef81286b..8db2676413 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -285,7 +285,7 @@ let rtauto_tac gls=
     begin
       reset_info ();
       if !verbose then
-	msgnl (str "Starting proof-search ...");
+	msg_info (str "Starting proof-search ...");
     end in
   let search_start_time = System.get_time () in
   let prf =
@@ -295,10 +295,10 @@ let rtauto_tac gls=
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof tree found in " ++
+      msg_info (str "Proof tree found in " ++
 	     System.fmt_time_difference search_start_time search_end_time);
       pp_info ();
-      msgnl (str "Building proof term ... ")
+      msg_info (str "Building proof term ... ")
     end in
   let build_start_time=System.get_time () in
   let _ = step_count := 0; node_count := 0 in
@@ -311,7 +311,7 @@ let rtauto_tac gls=
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof term built in " ++
+      msg_info (str "Proof term built in " ++
 	     System.fmt_time_difference build_start_time build_end_time ++
 	     fnl () ++
 	     str "Proof size : " ++ int !step_count ++
@@ -328,9 +328,9 @@ let rtauto_tac gls=
       Tactics.exact_no_check term gls in
   let tac_end_time = System.get_time () in
   let _ =
-    if !check then msgnl (str "Proof term type-checking is on");
+    if !check then msg_info (str "Proof term type-checking is on");
     if !verbose then
-      msgnl (str "Internal tactic executed in " ++
+      msg_info (str "Internal tactic executed in " ++
 	     System.fmt_time_difference tac_start_time tac_end_time) in
     result
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index a095c545f3..9b569a2b67 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -552,7 +552,7 @@ let ring_equality (r,add,mul,opp,req) =
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
-		    msgnl
+		    msg_info
 		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
@@ -561,7 +561,7 @@ let ring_equality (r,add,mul,opp,req) =
 		  op_morph)
             | None ->
 		(Flags.if_verbose
-		    msgnl
+		    msg_info
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index d09c7f05ad..916bced9eb 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -33,6 +33,8 @@ let explain_logic_error = ref (fun e -> mt())
 
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
+let msg_tac_debug s = Pp.ppnl s; Pp.pp_flush ()
+
 (* Prints the goal *)
 
 let db_pr_goal g =
@@ -44,12 +46,12 @@ let db_pr_goal g =
                    str" "  ++ pc) ++ fnl ()
 
 let db_pr_goal g =
-  msgnl (str "Goal:" ++ fnl () ++ db_pr_goal g)
+  msg_tac_debug (str "Goal:" ++ fnl () ++ db_pr_goal g)
 
 
 (* Prints the commands *)
 let help () =
-  msgnl (str "Commands: <Enter> = Continue" ++ fnl() ++
+  msg_tac_debug (str "Commands: <Enter> = Continue" ++ fnl() ++
          str "          h/? = Help" ++ fnl() ++
          str "          r <num> = Run <num> times" ++ fnl() ++
          str "          r <string> = Run up to next idtac <string>" ++ fnl() ++
@@ -60,7 +62,7 @@ let help () =
 let goal_com g tac =
   begin
     db_pr_goal g;
-    msgnl (str "Going to execute:" ++ fnl () ++ !prtac tac)
+    msg_tac_debug (str "Going to execute:" ++ fnl () ++ !prtac tac)
   end
 
 let skipped = ref 0
@@ -105,7 +107,7 @@ let run ini =
     for i=1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
-    msgnl (str "Executed expressions: " ++ int !skipped ++ fnl())
+    msg_tac_debug (str "Executed expressions: " ++ int !skipped ++ fnl())
   end;
   incr skipped
 
@@ -149,14 +151,14 @@ let debug_prompt lev g tac f =
 (* Prints a constr *)
 let db_constr debug env c =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str "Evaluated term: " ++ print_constr_env env c)
+    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
 
 (* Prints the pattern rule *)
 let db_pattern_rule debug num r =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
-    msgnl (str "Pattern rule " ++ int num ++ str ":");
-    msgnl (str "|" ++ spc () ++ !prmatchrl r)
+    msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
+      str "|" ++ spc () ++ !prmatchrl r)
   end
 
 (* Prints the hypothesis pattern identifier if it exists *)
@@ -167,39 +169,39 @@ let hyp_bound = function
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str "Hypothesis " ++
+    msg_tac_debug (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
                 " has been matched: ") ++ print_constr_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
+    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str "The goal has been successfully matched!" ++ fnl() ++
+    msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
+    msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            !prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
-    msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
+    msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++
            str "Let us try the next one...")
 
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     let s = str "message \"" ++ s ++ str "\"" in
-    msgnl
+    msg_tac_debug
       (str "This rule has failed due to \"Fail\" tactic (" ++
        s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
 
@@ -207,8 +209,8 @@ let db_eval_failure debug s =
 let db_logic_failure debug err =
   if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
-    msgnl (!explain_logic_error err);
-    msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
+    msg_tac_debug (!explain_logic_error err);
+    msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d62320e769..4553a8fa51 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -355,10 +355,10 @@ let hints_tac hints =
 	       | None -> aux i foundone tl
 	       | Some {it = gls; sigma = s'} ->
 	    	   if !typeclasses_debug then
-		     msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+		     msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 			    ++ str" on" ++ spc () ++ pr_ev s gl);
 		   let fk =
-		     (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ Lazy.force pp);
+		     (fun () -> if !typeclasses_debug then msg_debug (str"backtracked after " ++ Lazy.force pp);
 			aux (succ i) true tl)
 		   in
 		   let sgls =
@@ -393,7 +393,7 @@ let hints_tac hints =
 		     sk glsv fk)
 	| [] ->
 	  if not foundone && !typeclasses_debug then
-	    msgnl (pr_depth info.auto_depth ++ str": no match for " ++
+	    msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
 		     Printer.pr_constr_env (Goal.V82.env s gl) concl ++
 		     spc () ++ int (List.length poss) ++ str" possibilities");
 	  fk ()
@@ -424,7 +424,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 		  in
 		  let fk'' = 
 		    if not needs_backtrack then
-		      (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl ++ 
+		      (if !typeclasses_debug then msg_debug (str"no backtrack on " ++ pr_ev s gl ++ 
 							 str " after " ++ Lazy.force info.auto_last_tac); fk) 
 		    else fk' 
 		  in aux s' (gls'::acc) fk'' gls)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 599db8365c..8abb9c9e4e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -683,7 +683,7 @@ let  mkCaseEq a  : tactic =
 
 let case_eq_intros_rewrite x g =
   let n = nb_prod (Tacmach.pf_concl g) in
-  Pp.msgnl (Printer.pr_lconstr x); 
+  (* Pp.msgnl (Printer.pr_lconstr x); *)
   tclTHENLIST [
       mkCaseEq x;
       (fun g -> 
@@ -702,7 +702,7 @@ let rec find_a_destructable_match t =
 	  (* TODO check there is no rel n. *)
 	  raise (Found (Tacinterp.eval_tactic(<:tactic<destruct x>>)))
 	else
-	  let _ = Pp.msgnl (Printer.pr_lconstr x)  in
+	  (* let _ = Pp.msgnl (Printer.pr_lconstr x)  in *)
 	  raise (Found (case_eq_intros_rewrite x))
     | _ -> iter_constr find_a_destructable_match t
 	
@@ -714,8 +714,8 @@ let destauto t =
 
 let destauto_in id g = 
   let ctype = Tacmach.pf_type_of g (mkVar id) in
-  Pp.msgnl (Printer.pr_lconstr (mkVar id)); 
-  Pp.msgnl (Printer.pr_lconstr (ctype)); 
+(*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
+(*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype g
 
 TACTIC EXTEND destauto
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0bcc4ed47c..a628fe26a0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -58,10 +58,11 @@ open Miscops
 open Locus
 
 let safe_msgnl s =
-    try msgnl s with e ->
-      msgnl
-	(str "bug in the debugger: " ++
-         str "an exception is raised while printing debug information")
+  let _ =
+    try ppnl s with e ->
+    ppnl (str "bug in the debugger: an exception is raised while printing debug information")
+  in
+  pp_flush () 
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc
@@ -3148,7 +3149,7 @@ let add_tacdef local isrec tacl =
     | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl)) in
   List.iter
     (fun (id,b,_) ->
-      Flags.if_verbose msgnl (Libnames.pr_reference id ++
+      Flags.if_verbose msg_info (Libnames.pr_reference id ++
 				 (if b then str " is redefined"
 				   else str " is defined")))
     tacl
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