This patch splits pretty printing representation from IO operations.

8 files changed, 14 insertions, 14 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 451e0987b0..5d3c149ab9 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -1031,7 +1031,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ]
+| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ]
 END
 
 
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 0c25481d8e..308b6415d7 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -231,7 +231,7 @@ GEXTEND Gram
         Subterm (mode, oid, pc)
       | IDENT "appcontext";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        msg_warning (strbrk "appcontext is deprecated");
+        Feedback.msg_warning (strbrk "appcontext is deprecated");
         Subterm (true,oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
@@ -334,7 +334,7 @@ let vernac_solve n info tcom b =
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in
     p,status) in
-    if not status then Pp.feedback Feedback.AddedAxiom
+    if not status then Feedback.feedback Feedback.AddedAxiom
 
 let pr_ltac_selector = function
 | SelectNth i -> int i ++ str ":"
@@ -408,7 +408,7 @@ END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
+  [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
 
 let pr_ltac_ref = Libnames.pr_reference
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4
index 4cd8bf1feb..987b9d5387 100644
--- a/ltac/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
@@ -121,7 +121,7 @@ open Pp
 
 VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
 | [ "Show" "Obligation" "Tactic" ] -> [
-    msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
+    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -130,8 +130,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ]
-| [ "Preterm" ] -> [ msg_info (show_term None) ]
+| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ]
+| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ]
 END
 
 open Pp
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 395c2cd1b6..29ffbed196 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -262,5 +262,5 @@ TACTIC EXTEND setoid_transitivity
 END
 
 VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-  [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Pp.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
+  [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
 END
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index ddbd818bf4..1d9e7b34e8 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -435,7 +435,7 @@ let register_ltac local tacl =
           with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
         in
         let () = if is_primitive then
-          msg_warning (str "The Ltac name " ++ id_pp ++
+          Feedback.msg_warning (str "The Ltac name " ++ id_pp ++
             str " may be unusable because of a conflict with a notation.")
         in
         NewTac id, body
@@ -473,10 +473,10 @@ let register_ltac local tacl =
   let iter (def, tac) = match def with
   | NewTac id ->
     Tacenv.register_ltac false local id tac;
-    Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined")
+    Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined")
   | UpdateTac kn ->
     Tacenv.redefine_ltac local kn tac;
     let name = Nametab.shortest_qualid_of_tactic kn in
-    Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined")
+    Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
   List.iter iter defs
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index 39db6268b5..005d1f5f48 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -54,7 +54,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
         let () = tac_tab := MLTacMap.remove s !tac_tab in
-        msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
+        Feedback.msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
       else
         Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 5d282a6936..406fd41ad8 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1242,7 +1242,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
   | TacArg a -> interp_tactic ist (TacArg a)
   | TacInfo tac ->
-      msg_warning
+      Feedback.msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
 	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 1326818fc8..3f504b7f37 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -93,7 +93,7 @@ let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
    if not (eq_constr (Universes.constr_of_global ref') t') then
-    msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
+    Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
    ref'