This patch splits pretty printing representation from IO operations.

5 files changed, 15 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6b58baa997..e57b48e9e0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -229,11 +229,11 @@ let tclLOG (dbg,depth,trace) pp tac =
       Proofview.V82.tactic begin fun gl ->
 	try
 	  let out = Proofview.V82.of_tactic tac gl in
-	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+	  Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
 	  out
 	with reraise ->
           let reraise = Errors.push reraise in
-	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+	  Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
 	  iraise reraise
       end
     | Info ->
@@ -289,10 +289,10 @@ let tclTRY_dbg d tac =
   let delay f = Proofview.tclUNIT () >>= fun () -> f () in
   let tac = match level with
   | Off -> tac
-  | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
+  | Debug | Info -> delay (fun () -> Feedback.msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
   in
   let after = match level with
-  | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ())
+  | Info -> delay (fun () -> Feedback.msg_debug (pr_info_nop d); Proofview.tclUNIT ())
   | Off | Debug -> Proofview.tclUNIT ()
   in
   Tacticals.New.tclORELSE0 tac after
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index cfbcc47505..95b26c2d50 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -455,7 +455,7 @@ let hints_tac hints =
 	  | None -> aux i foundone tl
 	  | Some {it = gls; sigma = s';} ->
 	    if !typeclasses_debug then
-	      msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+	      Feedback.msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 			 ++ str" on" ++ spc () ++ pr_ev s gl);
 	    let sgls =
 	      evars_to_goals
@@ -504,7 +504,7 @@ let hints_tac hints =
 		in
 		let e' = match foundone with None -> e | Some e' -> merge_failures e e' in
 		  if !typeclasses_debug then
-		    msg_debug 
+		    Feedback.msg_debug 
 		      ((if do_backtrack then str"Backtracking after "
 			else str "Not backtracking after ")
 		       ++ Lazy.force pp);
@@ -514,7 +514,7 @@ let hints_tac hints =
 	      sk glsv fk')
       | [] ->
 	if foundone == None && !typeclasses_debug then
-	  msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
+	  Feedback.msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
 		       Printer.pr_constr_env (Goal.V82.env s gl) s concl ++
 		       spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities");
 	match foundone with
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index f0f408c24d..2cae9b7946 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -344,13 +344,13 @@ let mk_eauto_dbg d =
   else Off
 
 let pr_info_nop = function
-  | Info -> msg_debug (str "idtac.")
+  | Info -> Feedback.msg_debug (str "idtac.")
   | _ -> ()
 
 let pr_dbg_header = function
   | Off -> ()
-  | Debug -> msg_debug (str "(* debug eauto : *)")
-  | Info -> msg_debug (str "(* info eauto : *)")
+  | Debug -> Feedback.msg_debug (str "(* debug eauto : *)")
+  | Info  -> Feedback.msg_debug (str "(* info eauto : *)")
 
 let pr_info dbg s =
   if dbg != Info then ()
@@ -361,7 +361,7 @@ let pr_info dbg s =
 	| State sp ->
 	  let mindepth = loop sp in
 	  let indent = String.make (mindepth - sp.depth) ' ' in
-	  msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+	  Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
 	  mindepth
     in
     ignore (loop s)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index b2104ba433..b543b564c3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -692,7 +692,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    msg_warning (str "the hint: eapply " ++ pr_lconstr c ++
+	    Feedback.msg_warning (str "the hint: eapply " ++ pr_lconstr c ++
 	    str " will only be used by eauto");
           (Some hd,
            { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
@@ -1336,7 +1336,7 @@ let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
 let warn h x =
   let hint = pr_hint h in
   let (mp, _, _) = KerName.repr h.uid in
-  let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
+  let () = Feedback.msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
   Proofview.tclUNIT x
 
 let run_hint tac k = match !warn_hint with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15e9d3a943..a2431f6eff 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1307,7 +1307,7 @@ let enforce_prop_bound_names rename tac =
             mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
         | LetIn (na,c,t,t') ->
             mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
-        | _ -> print_int i; Pp.msg (print_constr t); assert false in
+        | _ -> print_int i; Feedback.msg_notice (print_constr t); assert false in
       let rename_branch i =
         Proofview.Goal.nf_enter { enter = begin fun gl ->
           let env = Proofview.Goal.env gl in
@@ -2939,7 +2939,7 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
 let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then
-    msg_warning
+    Feedback.msg_warning
       (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
        ++ str": " ++ prlist_with_sep spc 
 	 (Miscprint.pr_intro_pattern