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

21 files changed, 81 insertions, 84 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 699f1f3df..6fda2284a 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 78dbee3fe..2d017f5cf 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 7940009c6..204af93d5 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 2c845ce32..f10700736 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 c846d2d0f..a1c9898f2 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 fe86e1ae1..aa1e36f67 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 0efdbbb6b..62ce89896 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 978760e8e..185aa03ee 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 b6a0ef4c3..b009107dc 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 467080531..3aa57578d 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 269439a53..1d48ef45b 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 9f13e54cf..e7d05d5a9 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 046b65ee8..bd5fd9c09 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 21f77e438..42e5c36a8 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 a169c2826..7b341e581 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 026b9ad0e..8443959b4 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 b463b6c27..7745996c5 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 5fcd495ef..7cf438e6f 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 a1ab6cd30..46d561ed8 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 60ef81286..8db267641 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 a095c545f..9b569a2b6 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 \""++