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

3 files changed, 14 insertions, 13 deletions

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