Feedback cleanup

This patch splits pretty printing representation from IO operations.

- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.

The patch continues work initiated for 8.5 and has the following effects:

- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
  `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
  `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
  used instead.

- Feedback provides different backends to handle output, currently,
  `stdout`, `emacs` and CoqIDE backends are provided.

- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
  gone.

- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
  mix.

Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.

132 files changed, 813 insertions, 809 deletions

diff --git a/_tags b/_tags
index f805eeaa3..e8317d614 100644
--- a/_tags
+++ b/_tags
@@ -67,6 +67,7 @@
 "pretyping": include
 "printing": include
 "proofs": include
+"stm": include
 "tactics": include
 "theories": include
 "tools": include
diff --git a/checker/check.ml b/checker/check.ml
index 3a5c91217..93eb2a0d2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -111,15 +111,14 @@ 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 ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Admitting library: " ++ pr_dirpath dir);
       Safe_typing.unsafe_import file md m.library_extra_univs dig)
   else
-    (Flags.if_verbose ppnl
+    (Flags.if_verbose Feedback.msg_notice
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md m.library_extra_univs dig);
-  Flags.if_verbose pp (fnl());
-  pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (fnl());
   register_loaded_library m
 
 (*************************************************************************)
@@ -173,7 +172,7 @@ let remove_load_path dir =
 
 let add_load_path (phys_path,coq_path) =
   if !Flags.debug then
-    ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+    Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = canonical_path_name phys_path in
   let physical, logical = !load_paths in
@@ -188,7 +187,7 @@ let add_load_path (phys_path,coq_path) =
 	    begin
               (* Assume the user is concerned by library naming *)
 	      if dir <> default_root_prefix then
-		msg_warning
+		Feedback.msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
 		   pr_dirpath coq_path);
@@ -299,7 +298,7 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
       let ch = System.with_magic_number_check raw_intern_library f in
@@ -323,7 +322,7 @@ let intern_from_file (dir, f) =
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
-        pp (str " (was a vio file) ");
+       Feedback.msg_notice(str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
         errorlabstrm "intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
@@ -334,12 +333,12 @@ let intern_from_file (dir, f) =
       Validate.validate !Flags.debug Values.v_libsum sd;
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;
-      Flags.if_verbose ppnl (str" done]"); pp_flush ();
+      Flags.if_verbose Feedback.msg_notice (str" done]");
       let digest =
         if opaque_csts <> None then Cic.Dviovo (digest,udg)
         else (Cic.Dvo digest) in
       sd,md,table,opaque_csts,digest
-    with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
+    with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
   Option.iter (fun (opaque_csts,_,_) ->
@@ -407,11 +406,11 @@ let recheck_library ~norec ~admit ~check =
   let nochk =
     List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
   (* *)
-  Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose Feedback.msg_notice (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 ppnl (str"Modules were successfully checked")
+  Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 900cfe0c8..a093fd959 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -22,16 +22,18 @@ CList
 CString
 Serialize
 Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
 CObj
 CArray
 CStack
 Util
+Pp
 Ppstyle
+Xml_datatype
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
 Errors
 CEphemeron
 Future
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 84f5684d4..a26c93a30 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -57,12 +57,13 @@ let print_context env =
          env_modules=mods; env_modtypes=mtys};
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
-    ppnl(hov 0
+    Feedback.msg_notice
+      (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
-      fnl())); pp_flush()
+       fnl()));
   end
 
 let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 91a207a60..61b13c60b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -17,7 +17,7 @@ open Check
 let () = at_exit flush_all
 
 let fatal_error info anomaly =
-  flush_all (); pperrnl info; flush_all ();
+  flush_all (); Feedback.msg_error info; flush_all ();
   exit (if anomaly then 129 else 1)
 
 let coq_root = Id.of_string "Coq"
@@ -67,12 +67,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
       Check.add_load_path (dir,coq_dirpath)
     end
   else
-    msg_warning (str "Cannot open " ++ str dir)
+    Feedback.msg_warning (str "Cannot open " ++ str dir)
 
 let convert_string d =
   try Id.of_string d
   with Errors.UserError _ ->
-    if_verbose msg_warning
+    if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root =
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -123,7 +123,7 @@ let init_load_path () =
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
-    (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
+    (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
   (* then directories in COQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
@@ -288,7 +288,7 @@ let rec explain_exn = function
           Format.printf "@\nis not convertible with@\n";
           Print.print_pure_constr a;
           Format.printf "@\n====== universes ====@\n";
-          Pp.pp (Univ.pr_universes
+          Feedback.msg_notice (Univ.pr_universes
             (ctx.Environ.env_stratification.Environ.env_universes));
           str "\nCantApplyBadType at argument " ++ int n
       | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
diff --git a/checker/closure.ml b/checker/closure.ml
index c2708e97d..cef1d31a6 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() =
-  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  Feedback.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 fd5eaeb8b..a667bb8a3 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
 (************************************************************************)
 
 let check_inductive env kn mib =
-  Flags.if_verbose ppnl (str "  checking ind: " ++ MutInd.print kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
   let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index c07a35e35..7f93e1560 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
     | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
-  Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
+  Flags.if_verbose Feedback.msg_notice (str "  checking cst: " ++ prcon kn);
   let env' =
     if cb.const_polymorphic then
       let inst = Univ.make_abstract_instance cb.const_universes in
diff --git a/checker/print.ml b/checker/print.ml
index da8a6106f..c0d1ac368 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,7 @@ open Format
 open Cic
 open Names
 
-let print_instance i = Pp.pp (Univ.Instance.pr i)
+let print_instance i = Feedback.msg_notice (Univ.Instance.pr i)
 
 let print_pure_constr csr =
   let rec term_display c = match  c with
@@ -108,7 +108,7 @@ let print_pure_constr csr =
   and sort_display = function
     | Prop(Pos) -> print_string "Set"
     | Prop(Null) -> print_string "Prop"
-    | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")"
+    | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")"
 
   and name_display = function
     | Name id -> print_string (Id.to_string id)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7f9ed92f9..1071e2f93 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -81,7 +81,7 @@ let stamp_library file digest = ()
    warning is issued in case of mismatch *)
 let import file clib univs digest =
   let env = !genv in
-  check_imports msg_warning clib.comp_name env clib.comp_deps;
+  check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   let mb = clib.comp_mod in
   Mod_checking.check_module
@@ -93,7 +93,7 @@ let import file clib univs digest =
 (* When the module is admitted, digests *must* match *)
 let unsafe_import file clib univs digest =
   let env = !genv in
-  if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps
+  if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
   else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2f631c633..53497ff0e 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,69 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Logging and Pretty Printing: **
+
+* Printing functions have been removed from `Pp.mli`, which is now a
+  purely pretty-printing interface. Functions affected are:
+
+```` ocaml
+val pp          : std_ppcmds -> unit
+val ppnl        : std_ppcmds -> unit
+val pperr       : std_ppcmds -> unit
+val pperrnl     : std_ppcmds -> unit
+val pperr_flush : unit -> unit
+val pp_flush    : unit -> unit
+val flush_all   : unit -> unit
+val msg         : std_ppcmds -> unit
+val msgnl       : std_ppcmds -> unit
+val msgerr      : std_ppcmds -> unit
+val msgerrnl    : std_ppcmds -> unit
+val message     : string -> unit
+````
+
+  which are no more available. Users of `Pp.pp msg` should now use the
+  proper `Feedback.msg_*` function. Clients also have no control over
+  flushing, the back end takes care of it.
+
+* Feedback related functions and definitions have been moved to the
+  `Feedback` module. `message_level` has been renamed to
+  level. Functions moved from Pp to Feedback are:
+
+```` ocaml
+val set_logger      : logger -> unit
+val std_logger      : logger
+val emacs_logger    : logger
+val feedback_logger : logger
+````
+
+* We now provide several loggers, `log_via_feedback` is removed in
+  favor of `set_logger feedback_logger`. Output functions are:
+
+```` ocaml
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val msg_info    : Pp.std_ppcmds -> unit
+val msg_notice  : Pp.std_ppcmds -> unit
+val msg_warning : Pp.std_ppcmds -> unit
+val msg_error   : Pp.std_ppcmds -> unit
+val msg_debug   : Pp.std_ppcmds -> unit
+````
+
+  with the `msg_*` functions being just an alias for `logger $Level`.
+
+* The main feedback functions are:
+
+```` ocaml
+val set_feeder : (feedback -> unit) -> unit
+val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+````
+  Note that `feedback` doesn't take two parameters anymore. After
+  refactoring the following function has been removed:
+
+```` ocaml
+val get_id_for_feedback : unit -> edit_or_state_id * route_id
+````
+
 - The interface of the Context module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
diff --git a/dev/printers.mllib b/dev/printers.mllib
index aa74cb508..0957197cc 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -26,16 +26,17 @@ Control
 Loc
 Serialize
 Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
 CObj
 CArray
 CStack
 Util
+Pp
 Ppstyle
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
 Errors
 Bigint
 CUnix
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f5599d793..4da901e53 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,7 +29,8 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
 (* std_ppcmds *)
-let pppp x = pp x
+let pp   x = Feedback.msg_notice x
+let pppp x = Feedback.msg_notice x
 
 (** Future printer *)
 
@@ -315,7 +316,7 @@ let constr_display csr =
     | Anonymous -> "Anonymous"
 
   in
-  Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush ()
+  Feedback.msg_notice (str (term_display csr) ++fnl ())
 
 open Format;;
 
@@ -515,7 +516,7 @@ let _ =
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Errors.print e)
+    e -> Feedback.msg_notice (Errors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
@@ -531,7 +532,7 @@ let _ =
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Pp.pp (Errors.print e)
+    e -> Feedback.msg_notice (Errors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 1c501df80..afa94a63e 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -79,7 +79,7 @@ and ppwhd whd =
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
-  | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl)
+  | Vuniv_level lvl -> Feedback.msg_notice (Univ.Level.pr lvl)
 
 and ppvblock b =
   open_hbox();
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index d67f1eee3..64be07b9c 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -104,11 +104,11 @@ struct
       Util.iraise (Exception e, info)
 
   (** Use the current logger. The buffer is also flushed. *)
-  let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_info s =  make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
-  let print_warning s =  make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
-  let print_error s =  make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
-  let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
+  let print_debug   s = make (fun _ -> Feedback.msg_info s)
+  let print_info    s = make (fun _ -> Feedback.msg_info s)
+  let print_warning s = make (fun _ -> Feedback.msg_warning s)
+  let print_error   s = make (fun _ -> Feedback.msg_error s)
+  let print_notice  s = make (fun _ -> Feedback.msg_notice s)
 
   let run = fun x ->
     try x () with Exception e as src ->
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 45af16759..bcdd4da11 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
        evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
-  msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
+  Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
   new_el, { pv with solution = new_solution; }
 
 
@@ -857,7 +857,7 @@ let tclTIME s t =
       else
         str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking")
     in
-    msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
+    Feedback.msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++
              System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in
   let rec aux n t =
     let open Proof in
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 4c4ecaf73..0791306c4 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -117,7 +117,7 @@ let declare_tactic loc s c cl = match cl with
         Tacenv.register_ml_tactic $se$ [|$tac$|];
         Mltop.declare_cache_obj obj $plugin_name$; }
       with [ e when Errors.noncritical e ->
-        Pp.msg_warning
+        Feedback.msg_warning
           (Pp.app
             (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
             (Errors.print e)) ]; } >>
@@ -135,7 +135,7 @@ let declare_tactic loc s c cl = match cl with
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
         Mltop.declare_cache_obj $obj$ $plugin_name$; }
       with [ e when Errors.noncritical e ->
-        Pp.msg_warning
+        Feedback.msg_warning
           (Pp.app
             (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
             (Errors.print e)) ]; } >>
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 904662ea1..4060af8e4 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -128,7 +128,7 @@ let declare_command loc s c nt cl =
           CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
           CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ }
 	with [ e when Errors.noncritical e ->
-	  Pp.msg_warning
+	  Feedback.msg_warning
 	    (Pp.app
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
 	       (Errors.print e)) ];
diff --git a/ide/coq.ml b/ide/coq.ml
index fa0adf979..7a32faffc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -291,17 +291,17 @@ let rec check_errors = function
 | `OUT :: _ -> raise (TubeError "OUT")
 
 let handle_intermediate_message handle xml =
-  let message = Pp.to_message xml in
-  let level = message.Pp.message_level in
-  let content = message.Pp.message_content in
+  let message = Feedback.to_message xml in
+  let level = message.Feedback.message_level in
+  let content = message.Feedback.message_content in
   let logger = match handle.waiting_for with
     | Some (_, l) -> l 
     | None -> function
-        | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s)
-        | Pp.Info -> fun s -> Minilib.log ~level:`INFO  (xml_to_string s)
-        | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
-        | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING  (xml_to_string s)
-        | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
+        | Feedback.Error   -> fun s -> Minilib.log ~level:`ERROR   (xml_to_string s)
+        | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
+        | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
+        | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
+        | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
   in
   logger level (Richpp.richpp_of_xml content)
 
@@ -335,7 +335,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     let l_end = Lexing.lexeme_end lex in
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
-    if Pp.is_message xml then begin
+    if Feedback.is_message xml then begin
       handle_intermediate_message handle xml;
       loop ()
     end else if Feedback.is_feedback xml then begin
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index b55786ddd..930135995 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -519,7 +519,7 @@ object(self)
       self#position_error_tag_at_iter start phrase loc;
       buffer#place_cursor ~where:stop;
       messages#clear;
-      messages#push Pp.Error msg;
+      messages#push Feedback.Error msg;
       self#show_goals
     end else
       self#show_goals_aux ~move_insert:true ()
@@ -595,7 +595,8 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+
+            logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
@@ -611,7 +612,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Pp.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Richpp.richpp_of_string msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -619,7 +620,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Pp.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Richpp.richpp_of_string msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -638,7 +639,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+         messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status ~logger:messages#push true) next
@@ -740,8 +741,8 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC");
-          messages#push Pp.Error msg;
+          if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC");
+          messages#push Feedback.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
                  (Doc.focused document && Doc.is_in_focus document safe_id))
@@ -759,7 +760,7 @@ object(self)
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
     messages#clear;
-    messages#push Pp.Error msg;
+    messages#push Feedback.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1fe393d2b..758a5a4c9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -783,7 +783,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Pp.Error (Richpp.richpp_of_string msg)
+        sn.messages#push Feedback.Error (Richpp.richpp_of_string msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9a3e85e47..59efc2d82 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -98,11 +98,11 @@ let coqide_cmd_checks (loc,ast) =
   if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
-    msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
+    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
-    msg_warning (strbrk "Rather use CoqIDE navigation instead");
+    Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
   if is_query ast then
-    msg_warning (strbrk "Query commands should not be inserted in scripts")
+    Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
@@ -212,7 +212,7 @@ let export_pre_goals pgs =
 let goals () =
   Stm.finish ();
   let s = read_stdout () in
-  if not (String.is_empty s) then msg_info (str s);
+  if not (String.is_empty s) then Feedback.msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
@@ -222,7 +222,7 @@ let evars () =
   try
     Stm.finish ();
     let s = read_stdout () in
-    if not (String.is_empty s) then msg_info (str s);
+    if not (String.is_empty s) then Feedback.msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in
@@ -255,7 +255,7 @@ let status force =
   Stm.finish ();
   if force then Stm.join ();
   let s = read_stdout () in
-  if not (String.is_empty s) then msg_info (str s);
+  if not (String.is_empty s) then Feedback.msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -445,11 +445,11 @@ let slave_logger xml_oc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
   let message = {
-    Pp.message_level = level;
-    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
+    Feedback.message_level = level;
+    Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
   let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
-  let xml = Pp.of_message message in
+  let xml = Feedback.of_message message in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
@@ -471,8 +471,8 @@ let loop () =
     CThread.thread_friendly_read in_ch s ~off:0 ~len) in
   let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
-  set_logger (slave_logger xml_oc);
-  set_feeder (slave_feeder xml_oc);
+  Feedback.set_logger (slave_logger xml_oc);
+  Feedback.set_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -482,7 +482,7 @@ let loop () =
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
       let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in
+      let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
       print_xml xml_oc (Xmlprotocol.of_answer q r);
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 508881cad..00c3f88e5 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -297,15 +297,15 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Pp.message_level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
-  | Pp.Debug _ -> `DEBUG
-  | Pp.Info -> `INFO
-  | Pp.Notice -> `NOTICE
-  | Pp.Warning -> `WARNING
-  | Pp.Error -> `ERROR
+  | Feedback.Debug _ -> `DEBUG
+  | Feedback.Info -> `INFO
+  | Feedback.Notice -> `NOTICE
+  | Feedback.Warning -> `WARNING
+  | Feedback.Error -> `ERROR
   in
   Minilib.log ~level (xml_to_string message)
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 4e35a6f9f..491e8e823 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -69,7 +69,7 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Pp.message_level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Richpp.richpp -> unit
 
 val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 081094e2b..de0720e03 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -56,24 +56,24 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | ("-full"|"-opt") :: r ->
     process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
-    Pp.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
+    Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
     process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
   | "-no-install" :: r ->
-    Pp.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
+    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
     process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
   | "-install" :: d :: r ->
-    if install <> UnspecInstall then Pp.msg_warning (Pp.str "-install sets more than once.");
+    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
     let install =
       match d with
 	| "user" -> UserInstall
 	| "none" -> NoInstall
 	| "global" -> TraditionalInstall
-	| _ -> Pp.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
+	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
           install
     in
     process_cmd_line orig_dir (project_file,makefile,install,opt) l r
   | "-custom" :: com :: dependencies :: file :: r ->
-    Pp.msg_warning (Pp.app
+    Feedback.msg_warning (Pp.app
     (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
     (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
     );
@@ -94,7 +94,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match project_file with
       | None -> ()
-      | Some _ -> Pp.msg_warning (Pp.str
+      | Some _ -> Feedback.msg_warning (Pp.str
 	"Several features will not work with multiple project files.")
     in
     let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
@@ -109,7 +109,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
 	let () = match makefile with
 	  |None -> ()
 	  |Some f ->
-	     Pp.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
+	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
 	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
       end
   | v :: "=" :: def :: r ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 7728ad236..758f383d6 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -73,8 +73,8 @@ let message_view () : message_view =
 
     method push level msg =
       let tags = match level with
-      | Pp.Error -> [Tags.Message.error]
-      | Pp.Warning -> [Tags.Message.warning]
+      | Feedback.Error -> [Tags.Message.error]
+      | Feedback.Warning -> [Tags.Message.warning]
       | _ -> []
       in
       let rec non_empty = function
@@ -88,7 +88,7 @@ let message_view () : message_view =
         push#call (level, msg)
       end
 
-    method add msg = self#push Pp.Notice msg
+    method add msg = self#push Feedback.Notice msg
 
     method add_string s = self#add (Richpp.richpp_of_string s)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0de98242a..4a451634d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1069,7 +1069,7 @@ let alias_of als = match als.alias_ids with
 | id :: _ -> Name id
 
 let message_redundant_alias id1 id2 =
-  msg_warning
+  Feedback.msg_warning
     (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
 
 (** {6 Expanding notations }
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 85212b7ab..931fc1ca4 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -141,7 +141,7 @@ let interval loc =
 let dump_ref loc filepath modpath ident ty =
   match !glob_output with
   | Feedback ->
-    Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
+    Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
   | NoGlob -> ()
   | _ when not (Loc.is_ghost loc) ->
     let bl,el = interval loc in
@@ -240,7 +240,7 @@ let dump_binding loc id = ()
 
 let dump_def ty loc secpath id =
   if !glob_output = Feedback then
-    Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty))
+    Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
   else
     let bl,el = interval loc in
     dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 751b03a4a..567150a5d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -310,7 +310,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
 	  else
             let () = match bk with
             | Implicit ->
-	       msg_warning (strbrk "Ignoring implicit status of product binder " ++ 
+	       Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ 
 			      pr_name na ++ strbrk " and following binders")
             | _ -> ()
             in []
diff --git a/interp/notation.ml b/interp/notation.ml
index 0a65dfc09..b19fd9e1f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -184,7 +184,7 @@ let declare_delimiters scope key =
     | None -> scope_map := String.Map.add scope newsc !scope_map
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
-	msg_warning
+	Feedback.msg_warning
 	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
   end;
@@ -192,7 +192,7 @@ let declare_delimiters scope key =
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+      Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
       delimiters_map := String.Map.add key scope !delimiters_map
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -201,7 +201,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
@@ -388,7 +388,7 @@ let declare_notation_interpretation ntn scopt pat df =
     let which_scope = match scopt with
     | None -> mt ()
     | Some _ -> str " in scope " ++ str scope in
-    msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+    Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
   let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
   let () = scope_map := String.Map.add scope sc !scope_map in
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index db548ec32..891b64fa1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -93,7 +93,7 @@ let is_verbose_compat () =
 let verbose_compat kn def = function
   | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
     let act =
-      if !verbose_compat_notations then msg_warning else errorlabstrm ""
+      if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm ""
     in
     let pp_def = match def with
       | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 42538925a..91099bbb1 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -132,7 +132,7 @@ let fold_constr_expr_with_binders g f n acc = function
 	fold_local_binders g f n'
 	  (fold_local_binders g f n acc t lb) c lb) l acc
   | CCoFix (loc,_,_) ->
-      msg_warning (strbrk "Capture check in multiple binders not done"); acc
+      Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 77eac9ee9..431c914c0 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -904,10 +904,10 @@ let compile fail_on_error ?universes:(universes=0) env c =
     in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
     (if !Flags.dump_bytecode then
-      Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+      Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/kernel/closure.ml b/kernel/closure.ml
index bf3801e54..65123108f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -45,7 +45,7 @@ let reset () =
   prune := 0
 
 let stop() =
-  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
 	 int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
 	 str"]")
diff --git a/kernel/names.ml b/kernel/names.ml
index e8226d3d3..9abc9842a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -36,7 +36,7 @@ struct
 
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Feedback.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 79e5d3af0..44cf21cff 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1863,7 +1863,7 @@ let compile_constant env sigma prefix ~interactive con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1878,11 +1878,11 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
       code, name
     | _ -> 
         let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 4ed926f1f..a0ff9e123 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -134,12 +134,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
   match compile ml_filename code with
   | (true, fn) ->
       begin
-        if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
+        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
         let t0 = Sys.time () in
         call_linker ~fatal:true prefix fn (Some upds);
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
@@ -149,7 +149,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
     let msg = "Native compiler is disabled, falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
+    Feedback.msg_warning (Pp.str msg);
     vm_conv cv_pb env t1 t2
   end
   else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4296b73ab..5b92e9554 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -73,20 +73,20 @@ let call_compiler ml_filename =
     ::"-w"::"a"
     ::include_dirs
     @ ["-impl"; ml_filename] in
-  if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
       | Unix.WEXITED n ->
-         Pp.(msg_warning (str "command exited with status " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
       | Unix.WSIGNALED n ->
-         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
       | Unix.WSTOPPED n ->
-         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Pp.(msg_warning (str (Unix.error_message e)));
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
@@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then Errors.error msg
-      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
   (try
@@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds =
    with Dynlink.Error e as exn ->
      let exn = Errors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
-     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 9d159be64..246b00da4 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) =
      let con = make_con mp empty_dirpath l in
      (if !Flags.debug then
 	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_constant_field (pre_env env) prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
 	let id = mb.mind_packets.(0).mind_typename in
 	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_mind_field prefix mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
@@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
@@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5bf369441..30a346c91 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -681,7 +681,7 @@ let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3839135a8..6bfd2457a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -167,8 +167,10 @@ let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
-  Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-	      
+  let open Feedback in
+  Option.iter (fun state_id ->
+      feedback ~id:(State state_id) Feedback.Complete)
+
 let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 89e833254..53db6f5be 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,7 +185,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
-    (Pp.msg_warning
+    (Feedback.msg_warning
       (Pp.str "Bytecode compilation failed, falling back to default conversion");
      Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
 			    full_transparent_state env univs t1 t2)
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85..d06d4b376 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -88,7 +88,7 @@ let load_aux_file_for vfile =
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
      Flags.if_verbose
-       Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+       Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
      empty_aux_file
 
 let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 3c1c5da33..c3ec4a696 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -28,13 +28,14 @@ CArray
 CStack
 Util
 Stateid
-Feedback
 Pp
 Ppstyle
+Xml_datatype
+Richpp
+Feedback
 Xml_lexer
 Xml_parser
 Xml_printer
-Richpp
 CUnix
 Envars
 Aux_file
diff --git a/lib/explore.ml b/lib/explore.ml
index 587db1156..aa7bddf2b 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct
       | [i] -> int i
       | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    msg_debug (h 0 (pp_rec p) ++ pp)
+    Feedback.msg_debug (h 0 (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 1a90685de..dce4372ec 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -9,7 +9,7 @@
 open Xml_datatype
 open Serialize
 
-type message_level =
+type level =
   | Debug of string
   | Info
   | Notice
@@ -17,7 +17,7 @@ type message_level =
   | Error
 
 type message = {
-  message_level : message_level;
+  message_level : level;
   message_content : xml;
 }
 
@@ -169,3 +169,129 @@ let is_feedback = function
   | _ -> false
 
 let default_route = 0
+
+(** Feedback and logging *)
+open Pp
+open Pp_control
+
+type logger = level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl          strm = msgnl_with !std_ft strm
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_str = str "Debug:"   ++ spc ()
+let info_str = mt ()
+let warn_str = str "Warning:" ++ spc ()
+let  err_str = str "Error:"   ++ spc ()
+
+let make_body quoter info s = quoter (hov 0 (info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err level msg = match level with
+  | Debug _ -> msgnl (make_body dbg  dbg_str msg)
+  | Info    -> msgnl (make_body dbg info_str msg)
+  | Notice  -> msgnl msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with !err_ft (make_body err warn_str msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str msg)
+
+(** Standard loggers *)
+let std_logger   = gen_logger (fun x -> x) (fun x -> x)
+
+(* Color logger *)
+let color_terminal_logger level strm =
+  let msg = Ppstyle.color_msg in
+  match level with
+  | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Info    -> msg !std_ft strm
+  | Notice  -> msg !std_ft strm
+  | Warning ->
+    let header = ("Warning", Ppstyle.warning_tag) in
+    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
+  | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+let logger       = ref std_logger
+let set_logger l = logger := l
+
+let msg_info    x = !logger Info x
+let msg_notice  x = !logger Notice x
+let msg_warning x = !logger Warning x
+let msg_error   x = !logger Error x
+let msg_debug   x = !logger (Debug "_") x
+
+(** Feeders *)
+let feeder = ref ignore
+let set_feeder f = feeder := f
+
+let feedback_id    = ref (Edit 0)
+let feedback_route = ref default_route
+
+let set_id_for_feedback ?(route=default_route) i =
+  feedback_id := i; feedback_route := route
+
+let feedback ?id ?route what =
+  !feeder {
+     contents = what;
+     route = Option.default !feedback_route route;
+     id    = Option.default !feedback_id id;
+  }
+
+let feedback_logger lvl msg =
+  feedback ~route:!feedback_route ~id:!feedback_id (
+    Message {
+      message_level   = lvl;
+      message_content = Richpp.of_richpp (Richpp.richpp_of_pp msg);
+    })
+
+(* Output to file *)
+let ft_logger old_logger ft level mesg =
+  let id x = x in
+  match level with
+  | Debug _ -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Info    -> msgnl_with ft (make_body id info_str mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger level mesg
+  | Error   -> old_logger level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
+
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 0d8e20230..1e96f9a49 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -9,7 +9,7 @@
 open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
-type message_level =
+type level =
   | Debug of string
   | Info
   | Notice
@@ -17,7 +17,7 @@ type message_level =
   | Error
 
 type message = {
-  message_level : message_level;
+  message_level : level;
   message_content : xml;
 }
 
@@ -66,3 +66,80 @@ val of_feedback : feedback -> xml
 val to_feedback : xml -> feedback
 val is_feedback : xml -> bool
 
+(** {6 Feedback sent, even asynchronously, to the user interface} *)
+
+(** Moved here from pp.ml *)
+
+(* Morally the parser gets a string and an edit_id, and gives back an AST.
+ * Feedbacks during the parsing phase are attached to this edit_id.
+ * The interpreter assignes an exec_id to the ast, and feedbacks happening
+ * during interpretation are attached to the exec_id.
+ * Only one among state_id and edit_id can be provided. *)
+
+(** A [logger] takes a level plus a pretty printing doc and logs it *)
+type logger = level -> Pp.std_ppcmds -> unit
+
+(** [set_logger l] makes the [msg_*] to use [l] for logging *)
+val set_logger : logger -> unit
+
+(** [std_logger] standard logger to [stdout/stderr]  *)
+val std_logger : logger
+
+val color_terminal_logger : logger
+(* This logger will apply the proper {!Pp_style} tags, and in
+   particular use the formatters {!Pp_control.std_ft} and
+   {!Pp_control.err_ft} to display those messages. Be careful this is
+   not compatible with the Emacs mode!  *)
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger    : logger
+
+
+(** [set_feeder] A feeder processes the feedback, [ignore] by default *)
+val set_feeder : (feedback -> unit) -> unit
+
+(** [feedback ?id ?route fb] produces feedback fb, with [route] and
+    [id] set appropiatedly, if absent, it will use the defaults set by
+    [set_id_for_feedback] *)
+val feedback :
+  ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+
+(** [set_id_for_feedback route id] Set the defaults for feedback *)
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
+(** {6 output functions}
+
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
+interfaces use the xml-like protocol this constraint can be
+relaxed. *)
+(* Should we advertise these functions more? Should they be the ONLY
+   allowed way to output something? *)
+
+val msg_info : Pp.std_ppcmds -> unit
+(** Message that displays information, usually in verbose mode, such as [Foobar
+    is defined] *)
+
+val msg_notice : Pp.std_ppcmds -> unit
+(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
+
+val msg_warning : Pp.std_ppcmds -> unit
+(** Message indicating that something went wrong, but without serious
+    consequences. *)
+
+val msg_error : Pp.std_ppcmds -> unit
+(** Message indicating that something went really wrong, though still
+    recoverable; otherwise an exception would have been raised. *)
+
+val msg_debug : Pp.std_ppcmds -> unit
+(** For debugging purposes *)
+
+
+
+
diff --git a/lib/pp.ml b/lib/pp.ml
index e4c78ba73..d07f01b90 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -64,13 +64,6 @@ end
 
 open Pp_control
 
-(* This should not be used outside of this file. Use
-   Flags.print_emacs instead. This one is updated when reading
-   command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Flags] -> [Util] ->
-   [Pp] -> [Flags] *)
-let print_emacs = ref false
-
 (* The different kinds of blocks are:
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -339,175 +332,23 @@ let pp_dirs ?pp_tag ft =
       let () = Format.pp_print_flush ft () in
       Exninfo.iraise reraise
 
-
-
-(* pretty print on stdout and stderr *)
-
-(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_quote_start = String.make 1 (Char.chr 254)
-let emacs_quote_end = String.make 1 (Char.chr 255)
-
-let emacs_quote_info_start = "<infomsg>"
-let emacs_quote_info_end = "</infomsg>"
-
-let emacs_quote g =
-  if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
-  else hov 0 g
-
-let emacs_quote_info g =
-  if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
-  else hov 0 g
-
-
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ?pp_tag ft strm =
   pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
 
-let ppnl_with ft strm =
-  pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
-
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
   pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
 
-let msgnl_with ft strm =
-  pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_newline))
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp        x = pp_with   !std_ft x
-let ppnl      x = ppnl_with !std_ft x
-let pperr     x = pp_with   !err_ft x
-let pperrnl   x = ppnl_with !err_ft x
-let message   s = ppnl      (str s)
-let pp_flush  x = Format.pp_print_flush !std_ft x
-let pperr_flush x = Format.pp_print_flush !err_ft x
-let flush_all () =
-  flush stderr; flush stdout; pp_flush (); pperr_flush ()
-
-(* pretty printing functions WITH FLUSH *)
-let msg x = msg_with !std_ft x
-let msgnl x = msgnl_with !std_ft x
-let msgerr x = msg_with !err_ft x
-let msgerrnl x = msgnl_with !err_ft x
-
-(* Logging management *)
-
-type message_level =  Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : Xml_datatype.xml;
-}
-
-let of_message = Feedback.of_message
-let to_message = Feedback.to_message
-let is_message = Feedback.is_message
-
-type logger = message_level -> std_ppcmds -> unit
-
-let make_body info s =
-  emacs_quote (hov 0 (info ++ spc () ++ s))
-
-let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm))
-let warnbody strm = make_body (str "Warning:") strm
-let errorbody strm = make_body (str "Error:") strm
-let infobody strm = emacs_quote_info strm
-
-let std_logger ~id:_ level msg = match level with
-| Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
-| Notice -> msgnl msg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
-| Error -> msgnl_with !err_ft (errorbody msg)
-
-let emacs_logger ~id:_ level mesg = match level with
-| Debug _ -> msgnl (debugbody mesg)
-| Info -> msgnl (infobody mesg)
-| Notice -> msgnl mesg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) ()
-| Error -> msgnl_with !err_ft (errorbody mesg)
-
-let logger = ref std_logger
-
-let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
-let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
-
-let ft_logger old_logger ft ~id level mesg = match level with
-  | Debug _ -> msgnl_with ft (debugbody mesg)
-  | Info -> msgnl_with ft (infobody mesg)
-  | Notice -> msgnl_with ft mesg
-  | Warning -> old_logger ~id:id level mesg
-  | Error -> old_logger ~id:id level mesg
-
-let with_output_to_file fname func input =
-  let old_logger = !logger in
-  let channel = open_out (String.concat "." [fname; "out"]) in
-  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
-  try
-    let output = func input in
-    logger := old_logger;
-    close_out channel;
-    output
-  with reraise ->
-    let reraise = Backtrace.add_backtrace reraise in
-    logger := old_logger;
-    close_out channel;
-    Exninfo.iraise reraise
-
-let feedback_id = ref (Feedback.Edit 0)
-let feedback_route = ref Feedback.default_route
-
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
    them to different windows. *)
 
-let msg_info x = !logger ~id:!feedback_id Info x
-let msg_notice x = !logger ~id:!feedback_id Notice x
-let msg_warning x = !logger ~id:!feedback_id Warning x
-let msg_error x = !logger ~id:!feedback_id Error x
-let msg_debug x = !logger ~id:!feedback_id (Debug "_") x
-
-let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg)
-
-let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
-
-(** Feedback *)
-
-let feeder = ref ignore
-let set_id_for_feedback ?(route=Feedback.default_route) i =
-  feedback_id := i; feedback_route := route
-let feedback ?state_id ?edit_id ?route what =
-  !feeder {
-     Feedback.contents = what;
-     Feedback.route = Option.default !feedback_route route;
-     Feedback.id =
-       match state_id, edit_id with
-       | Some id, _ -> Feedback.State id
-       | None, Some eid -> Feedback.Edit eid
-       | None, None -> !feedback_id;
-  }
-let set_feeder f = feeder := f
-let get_id_for_feedback () = !feedback_id, !feedback_route
-
-(** Utility *)
-
+(** Output to a string formatter *)
 let string_of_ppcmds c =
-  msg_with Format.str_formatter c;
+  Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
   Format.flush_str_formatter ()
 
-let log_via_feedback printer = logger := (fun ~id lvl msg ->
-  !feeder {
-     Feedback.contents = Feedback.Message {
-       message_level = lvl;
-       message_content = printer msg };
-     Feedback.route = !feedback_route;
-     Feedback.id = id })
-
 (* Copy paste from Util *)
 
 let pr_comma () = str "," ++ spc ()
@@ -597,3 +438,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
+
diff --git a/lib/pp.mli b/lib/pp.mli
index 04a60a7c8..ced4b6603 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,32 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Modify pretty printing functions behavior for emacs ouput (special
-   chars inserted at some places). This function should called once in
-   module [Options], that's all. *)
-val make_pp_emacs:unit -> unit
-val make_pp_nonemacs:unit -> unit
-
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-
 (** Pretty-printers. *)
 
 type std_ppcmds
 
 (** {6 Formatting commands} *)
 
-val str  : string -> std_ppcmds
+val str   : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
-val brk : int * int -> std_ppcmds
-val tbrk : int * int -> std_ppcmds
-val tab : unit -> std_ppcmds
-val fnl : unit -> std_ppcmds
-val pifb : unit -> std_ppcmds
-val ws : int -> std_ppcmds
-val mt : unit -> std_ppcmds
-val ismt : std_ppcmds -> bool
-
-val comment : int -> std_ppcmds
+val brk   : int * int -> std_ppcmds
+val tbrk  : int * int -> std_ppcmds
+val tab   : unit -> std_ppcmds
+val fnl   : unit -> std_ppcmds
+val pifb  : unit -> std_ppcmds
+val ws    : int -> std_ppcmds
+val mt    : unit -> std_ppcmds
+val ismt  : std_ppcmds -> bool
+
+val comment  : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
 (** {6 Manipulation commands} *)
@@ -100,87 +92,10 @@ sig
   (** Project an object from a tag. *)
 end
 
-type tag_handler = Tag.t -> Format.tag
-
 val tag : Tag.t -> std_ppcmds -> std_ppcmds
 val open_tag : Tag.t -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
-(** {6 Sending messages to the user} *)
-type message_level = Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : Xml_datatype.xml;
-}
-
-type logger = message_level -> std_ppcmds -> unit
-
-(** {6 output functions}
-
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
-(* Should we advertise these functions more? Should they be the ONLY
-   allowed way to output something? *)
-
-val msg_info : std_ppcmds -> unit
-(** Message that displays information, usually in verbose mode, such as [Foobar
-    is defined] *)
-
-val msg_notice : std_ppcmds -> unit
-(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
-
-val msg_warning : std_ppcmds -> unit
-(** Message indicating that something went wrong, but without serious
-    consequences. *)
-
-val msg_error : std_ppcmds -> unit
-(** Message indicating that something went really wrong, though still
-    recoverable; otherwise an exception would have been raised. *)
-
-val msg_debug : std_ppcmds -> unit
-(** For debugging purposes *)
-
-val std_logger : logger
-(** Standard logging function *)
-
-val set_logger : logger -> unit
-
-val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
-
-val of_message : message -> Xml_datatype.xml
-val to_message : Xml_datatype.xml -> message
-val is_message : Xml_datatype.xml -> bool
-
-
-(** {6 Feedback sent, even asynchronously, to the user interface} *)
-
-(* This stuff should be available to most of the system, line msg_* above.
- * But I'm unsure this is the right place, especially for the global edit_id.
- *
- * Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assigns an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
-
-val feedback :
-  ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id ->
-  ?route:Feedback.route_id -> Feedback.feedback_content -> unit
-
-val set_id_for_feedback :
-  ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
-val set_feeder : (Feedback.feedback -> unit) -> unit
-val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id
-
 (** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
@@ -251,31 +166,9 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
-(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
-
-val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
+(** {6 Low-level pretty-printing functions with and without flush} *)
 
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
-
-(** These functions are low-level interface to printing and should not be used
-    in usual code. Consider using the [msg_*] function family instead. *)
-
-val pp : std_ppcmds -> unit
-val ppnl : std_ppcmds -> unit
-val pperr : std_ppcmds -> unit
-val pperrnl : std_ppcmds -> unit
-val pperr_flush : unit -> unit
-val pp_flush : unit -> unit
-val flush_all: unit -> unit
-
-(** {6 Deprecated functions} *)
-
-(** DEPRECATED. Do not use in newly written code. *)
-
-val msg_with : Format.formatter -> std_ppcmds -> unit
-
-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 *)
+(** FIXME: These ignore the logging settings and call [Format] directly *)
+type tag_handler = Tag.t -> Format.tag
+val msg_with :                        Format.formatter -> std_ppcmds -> unit
+val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index 3ecaac039..b068788c9 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with
 | None -> ""
 | Some key -> key
 
+let clear_tag_fn = ref (fun () -> ())
+
 let init_color_output () =
   let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+  clear_tag_fn := clear_tag;
   let tag_handler = {
     Format.mark_open_tag = push_tag;
     Format.mark_close_tag = pop_tag;
@@ -116,34 +119,23 @@ let init_color_output () =
     Format.print_close_tag = ignore;
   } in
   let open Pp_control in
-  let () = Format.pp_set_mark_tags !std_ft true in
-  let () = Format.pp_set_mark_tags !err_ft true in
-  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
-  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+let color_msg ?header ft strm =
   let pptag = tag in
   let open Pp in
-  let msg ?header ft strm =
-    let strm = match header with
+  let strm = match header with
     | None -> hov 0 strm
     | Some (h, t) ->
       let tag = Pp.Tag.inj t pptag in
       let h = Pp.tag tag (str h ++ str ":") in
       hov 0 (h ++ spc () ++ strm)
-    in
-    pp_with ~pp_tag ft strm;
-    Format.pp_print_newline ft ();
-    Format.pp_print_flush ft ();
-    (** In case something went wrong, we reset the stack *)
-    clear_tag ();
-  in
-  let logger level strm = match level with
-  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
-  | Info -> msg !std_ft strm
-  | Notice -> msg !std_ft strm
-  | Warning ->
-    let header = ("Warning", warning_tag) in
-    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
-  | Error -> msg ~header:("Error", error_tag) !err_ft strm
   in
-  let () = set_logger logger in
-  ()
+  pp_with ~pp_tag ft strm;
+  Format.pp_print_newline ft ();
+  Format.pp_print_flush ft ();
+  (** In case something went wrong, we reset the stack *)
+  !clear_tag_fn ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 97b5869f9..1cd701ed4 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -11,7 +11,8 @@
 
 (** {5 Style tags} *)
 
-type t
+type t = string
+
 (** Style tags *)
 
 val make : ?style:Terminal.style -> string list -> t
@@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list
 (** {5 Setting color output} *)
 
 val init_color_output : unit -> unit
-(** Once called, all tags defined here will use their current style when
-    printed. To this end, this function redefines the loggers used when sending
-    messages to the user. The program will in particular use the formatters
-    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
-    with additional syle information provided by this module. Be careful this is
-    not compatible with the Emacs mode! *)
+
+val color_msg : ?header:string * Format.tag ->
+  Format.formatter -> Pp.std_ppcmds -> unit
+(** {!color_msg ?header fmt pp} will format according to the tags
+     defined in this file *)
 
 val pp_tag : Pp.tag_handler
 (** Returns the name of a style tag that is understandable by the formatters
diff --git a/lib/system.ml b/lib/system.ml
index e54109a2f..8cdcaf5dc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -88,9 +88,9 @@ let all_subdirs ~unix_path:root =
       | _ -> ()
     in process_directory f path
   in
-  check_unix_dir (fun s -> msg_warning (str s)) root;
+  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
-  else msg_warning (str ("Cannot open " ^ root));
+  else Feedback.msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -149,7 +149,7 @@ let where_in_path ?(warn=true) path filename =
   | (lpe, f) :: l' ->
     let () = match l' with
     | _ :: _ when warn ->
-      msg_warning
+      Feedback.msg_warning
         (str filename ++ str " has been found in" ++ spc () ++
           hov 0 (str "[ " ++
             hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
@@ -205,7 +205,7 @@ let is_in_system_path filename =
     let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
     is_in_path lpath filename
   with Not_found ->
-    msg_warning (str "system variable PATH not found");
+    Feedback.msg_warning (str "system variable PATH not found");
     false
 
 let open_trapping_failure name =
@@ -216,7 +216,7 @@ let open_trapping_failure name =
 let try_remove filename =
   try Sys.remove filename
   with e when Errors.noncritical e ->
-    msg_warning
+    Feedback.msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let error_corrupted file s =
@@ -345,13 +345,13 @@ let with_time time f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if time then "" else " (successful)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if time then "" else "Finished failing transaction in " in
     let msg2 = if time then "" else " (failure)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 let process_id () =
diff --git a/library/declare.ml b/library/declare.ml
index c59d190a0..b0df32b8d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -398,7 +398,7 @@ let declare_mind mie =
 let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "no recursive definition")
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
@@ -413,7 +413,7 @@ let fixpoint_message indexes l =
 		    | None -> mt ()))
 
 let cofixpoint_message l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "No corecursive definition.")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -423,13 +423,13 @@ let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
 
 let assumption_message id =
   (* Changing "assumed" to "declared", "assuming" referring more to
   the type of the object than to the name of the object (see
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
-  Flags.if_verbose msg_info (pr_id id ++ str " is declared")
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 5f6512e11..4aa3a2a21 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -108,7 +108,8 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      pp (str table_name ++
+      Feedback.msg_notice
+        (str table_name ++
 	   (hov 0
 	      (if MySet.is_empty table then str " None" ++ fnl ()
                else MySet.fold
@@ -122,7 +123,7 @@ module MakeTable =
       method mem x =
 	let y = A.encode x in
         let answer = MySet.mem y !t in
-        msg_info (A.member_message y answer)
+        Feedback.msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
     end
 
@@ -271,7 +272,7 @@ let declare_option cast uncast
   in
   let warn () =
     if depr then
-      msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+      Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
   in
   let cread () = cast (read ()) in
   let cwrite v = warn (); write (uncast v) in
@@ -346,12 +347,12 @@ let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
   try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> msg_warning s
+  with UserError (_,s) -> Feedback.msg_warning s
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
   try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> msg_warning s
+  with UserError (_,s) -> Feedback.msg_warning s
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
@@ -375,9 +376,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+	Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+	Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
diff --git a/library/libobject.ml b/library/libobject.ml
index c566840e4..b12d2038a 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -133,7 +133,7 @@ let apply_dyn_fun deflt f lobj =
     Failure "local to_apply_dyn_fun" ->
       if not (!relax_flag || Hashtbl.mem missing_tab tag) then
         begin
-          Pp.msg_warning
+          Feedback.msg_warning
 	    (Pp.str ("Cannot find library functions for an object with tag "
                       ^ tag ^ " (a plugin may be missing)"));
           Hashtbl.add missing_tab tag ()
diff --git a/library/library.ml b/library/library.ml
index 8e2402dda..192700be7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -287,7 +287,7 @@ let locate_absolute_library dir =
   | [] -> raise LibNotFound
   | [file] -> file
   | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
          str vo ++ str " because it is more recent");
        vi
   | [vo;vi] -> vo
@@ -311,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
     | [lpath, file] -> lpath, file
     | [lpath_vo, vo; lpath_vi, vi]
       when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
          str vo ++ str " because it is more recent");
        lpath_vi, vi
     | [lpath_vo, vo; _ ] -> lpath_vo, vo
@@ -370,7 +370,7 @@ let access_table what tables dp i =
     | Fetched t -> t
     | ToFetch f ->
       let dir_path = Names.DirPath.to_string dp in
-      Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
       let t =
         try fetch_delayed f
         with Faulty f ->
@@ -448,7 +448,7 @@ let intern_from_file f =
 module DPMap = Map.Make(DirPath)
 
 let rec intern_library (needed, contents) (dir, f) from =
-  Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
+  Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
   (* Look if in the current logical environment *)
   try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
@@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
       (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
-  Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
+  Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
   m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
 
 and intern_library_deps libs dir m from =
@@ -755,7 +755,7 @@ let save_library_to ?todo dir f otab =
 	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = msg_warning (str "Removed file " ++ str f') in
+    let () = Feedback.msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
diff --git a/library/loadpath.ml b/library/loadpath.ml
index f8169576d..33c0f41e1 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit =
         let () =
           (* Do not warn when overriding the default "-I ." path *)
           if not (DirPath.equal old_path Nameops.default_root_prefix) then
-            msg_warning
+            Feedback.msg_warning
               (str phys_path ++ strbrk " was previously bound to " ++
                  pr_dirpath old_path ++ strbrk "; it is remapped to " ++
                  pr_dirpath coq_path) in
diff --git a/library/nametab.ml b/library/nametab.ml
index bbae98fc0..db902d625 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -119,7 +119,7 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		    msg_warning (str ("Trying to mask the absolute name \""
+		    Feedback.msg_warning (str ("Trying to mask the absolute name \""
 			     ^ U.to_string n ^ "\"!"));
 		  tree.path
 	      | Nothing
@@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function
         | Absolute (n,_) ->
             (* This is an absolute name, we must keep it
                 otherwise it may become unaccessible forever *)
-              msg_warning (str ("Trying to mask the absolute name \""
+              Feedback.msg_warning (str ("Trying to mask the absolute name \""
                         ^ U.to_string n ^ "\"!"));
             tree.path
         | Nothing
@@ -525,7 +525,7 @@ let shortest_qualid_of_tactic kn =
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
-    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
+    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 451e0987b..5d3c149ab 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 0c25481d8..308b6415d 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 4cd8bf1fe..987b9d538 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 395c2cd1b..29ffbed19 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 ddbd818bf..1d9e7b34e 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 39db6268b..005d1f5f4 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 5d282a693..406fd41ad 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 1326818fc..3f504b7f3 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'
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 8b8b38c34..9a7aeaf0c 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -199,7 +199,7 @@ let check_keyword str =
 let check_keyword_to_add s =
   try check_keyword s
   with Error.E (UnsupportedUnicode unicode) ->
-    Flags.if_verbose msg_warning
+    Flags.if_verbose Feedback.msg_warning
       (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
                                which will not be parsable." s unicode))
 
@@ -322,7 +322,7 @@ let rec string in_comments bp len = parser
         | [< '')'; s >] ->
             let () = match in_comments with
             | Some 0 ->
-                msg_warning
+                Feedback.msg_warning
                   (strbrk
                      "Not interpreting \"*)\" as the end of current \
                       non-terminated comment because it occurs in a \
@@ -389,9 +389,10 @@ let comment_stop ep =
     let bp = match !comment_begin with
         Some bp -> bp
       | None ->
-          msgerrnl(str "No begin location for comment '"
-                   ++ str current_s ++str"' ending at  "
-                   ++ int ep);
+          Feedback.msg_notice
+            (str "No begin location for comment '"
+             ++ str current_s ++str"' ending at  "
+             ++ int ep);
           ep-1 in
     Pp.comments := ((bp,ep),current_s) :: !Pp.comments);
   Buffer.clear current;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1a27d9692..87e27be69 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -473,10 +473,10 @@ GEXTEND Gram
     [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
         let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
-        msg_warning (strbrk msg); Some (!@loc, pat)
+        Feedback.msg_warning (strbrk msg); Some (!@loc, pat)
       | IDENT "_eqn" ->
         let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
-        msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
+        Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index df42d9084..0df15babd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -125,13 +125,13 @@ END
 
 let test_plural_form = function
   | [(_,([_],_))] ->
-      Flags.if_verbose msg_warning
+      Flags.if_verbose Feedback.msg_warning
    (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
   | _ -> ()
 
 let test_plural_form_types = function
   | [([_],_)] ->
-      Flags.if_verbose msg_warning
+      Flags.if_verbose Feedback.msg_warning
    (strbrk "Keywords Implicit Types expect more than one type")
   | _ -> ()
 
@@ -448,7 +448,7 @@ GEXTEND Gram
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  Flags.if_verbose
-            msg_warning (strbrk "Include Type is deprecated; use Include instead");
+            Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead");
           VernacInclude(e::l) ] ]
   ;
   export_token:
@@ -667,7 +667,7 @@ GEXTEND Gram
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
-        msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
+       Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
         VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
@@ -675,7 +675,7 @@ GEXTEND Gram
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   Flags.if_verbose
-             msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
+            Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
 	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 898dcd255..76db2f3c2 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
 let cc_verbose=ref false
 
 let debug x =
-  if !cc_verbose then msg_debug (x ())
+  if !cc_verbose then Feedback.msg_debug (x ())
 
 let _=
   let gdopt=
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c8924073c..bd788a425 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms =
 	      List.map
 		(build_term_to_complete uf newmeta)
 		(epsilons uf) in
-	    Pp.msg_info
+	    Feedback.msg_info
 	      (Pp.str "Goal is solvable by congruence but \
  some arguments are missing.");
-	    Pp.msg_info
+	    Feedback.msg_info
 	      (Pp.str "  Try " ++
 		 hov 8
 		 begin
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index be6ce59bd..3fa600ac2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -169,7 +169,7 @@ let do_daimon () =
       daimon_instr env p
     end
   in
-  if not status then Pp.feedback Feedback.AddedAxiom else ()
+  if not status then Feedback.feedback Feedback.AddedAxiom else ()
 
 (* post-instruction focus management *)
 
@@ -291,7 +291,7 @@ let justification tac gls=
 	   error "Insufficient justification."
 	 else
 	   begin
-	     msg_warning (str "Insufficient justification.");
+	     Feedback.msg_warning (str "Insufficient justification.");
 	     daimon_tac gls
 	   end) gls
 
@@ -1293,7 +1293,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	       end;
 	       match bro with
 		   None ->
-		     msg_warning (str "missing case");
+		     Feedback.msg_warning (str "missing case");
 		     tacnext (mkMeta 1)
 		 | Some (sub_ids,tree) ->
 		     let br_args =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 67c1c5901..a03be5743 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -541,7 +541,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 not (Int.equal (Buffer.length buf) 0) then begin
-    Pp.msg_notice (str (Buffer.contents buf));
+    Feedback.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -635,7 +635,7 @@ let simple_extraction r =
       in
       let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
       reset ();
-      Pp.msg_notice ans
+      Feedback.msg_notice ans
   | _ -> assert false
 
 
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index eb2f02244..0a8cb0ccd 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -101,7 +101,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
-  -> [ msg_info (print_extraction_inline ()) ]
+  -> [Feedback. msg_info (print_extraction_inline ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -123,7 +123,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
-  -> [ msg_info (print_extraction_blacklist ()) ]
+  -> [ Feedback.msg_info (print_extraction_blacklist ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f336941ee..560fe5aea 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -300,7 +300,7 @@ let warning_axioms () =
   if List.is_empty info_axioms then ()
   else begin
     let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
-    msg_warning
+    Feedback.msg_warning
       (str ("The following "^s^" must be realized in the extracted code:")
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
@@ -310,7 +310,7 @@ let warning_axioms () =
   else begin
     let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
     in
-    msg_warning
+    Feedback.msg_warning
       (str ("The following logical "^s^" encountered:") ++
        hov 1
          (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
@@ -326,12 +326,12 @@ let warning_opaques accessed =
   else
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
     if accessed then
-      msg_warning
+      Feedback.msg_warning
 	(str "The extraction is currently set to bypass opacity,\n" ++
 	 str "the following opaque constant bodies have been accessed :" ++
 	 lst ++ str "." ++ fnl ())
     else
-      msg_warning
+      Feedback.msg_warning
 	(str "The extraction now honors the opacity constraints by default,\n" ++
 	 str "the following opaque constants have been extracted as axioms :" ++
 	 lst ++ str "." ++ fnl () ++
@@ -339,7 +339,7 @@ let warning_opaques accessed =
 	 ++ fnl ())
 
 let warning_both_mod_and_cst q mp r =
- msg_warning
+ Feedback.msg_warning
    (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
     str "do you mean module " ++
     pr_long_mp mp ++
@@ -358,7 +358,7 @@ let check_inside_module () =
     err (str "You can't do that within a Module Type." ++ fnl () ++
 	 str "Close it and try again.")
   else if Lib.is_module () then
-    msg_warning
+    Feedback.msg_warning
       (str "Extraction inside an opened module is experimental.\n" ++
        str "In case of problem, close it first.\n")
 
@@ -368,7 +368,7 @@ let check_inside_section () =
 	 str "Close it and try again.")
 
 let warning_id s =
-  msg_warning (str ("The identifier "^s^
+  Feedback.msg_warning (str ("The identifier "^s^
 		    " contains __ which is reserved for the extraction"))
 
 let error_constant r =
@@ -449,7 +449,7 @@ let error_remaining_implicit k =
 
 let warning_remaining_implicit k =
   let s = msg_of_implicit k in
-  msg_warning
+  Feedback.msg_warning
     (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
      str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
      ++ str "but this code is potentially unsafe, please review it manually.")
@@ -465,7 +465,7 @@ let check_loaded_modfile mp = match base_mp mp with
   | _ -> ()
 
 let info_file f =
-  Flags.if_verbose msg_info
+  Flags.if_verbose Feedback.msg_info
     (str ("The file "^f^" has been created by extraction."))
 
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 134b6ba94..a78532e33 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -74,7 +74,7 @@ END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
 | [ "Print" "Firstorder" "Solver" ] -> [
-    Pp.msg_info
+    Feedback.msg_info
       (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
 END
 
@@ -131,7 +131,7 @@ ARGUMENT EXTEND firstorder_using
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
 | [ "using" reference(a) reference(b) reference_list(l) ] -> [
     Flags.if_verbose
-      Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+      Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
     a::b::l
   ]
 | [ ] -> [ [] ]
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 3b9f67f66..d7da85b4f 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -32,7 +32,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.msg_debug (Printer.pr_goal gl);
+    then Feedback.msg_debug (Printer.pr_goal gl);
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 879145c2f..52094cf08 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -52,17 +52,17 @@ let rec print_debug_queue e =
       let _ =
 	match e with
 	| Some e ->
-	   Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	   Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
 	| None ->
 	   begin
-	     Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
+	     Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
 	   end in
       print_debug_queue None ;
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.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 91a826c73..5b4fb2595 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -19,7 +19,7 @@ exception Toberemoved
 
 let observe s =
   if do_observe ()
-  then Pp.msg_debug s
+  then Feedback.msg_debug s
 
 (*
    Transform an inductive induction principle into
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6dfc23511..c63527dea 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -193,12 +193,12 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-	Pp.msg_warning
+	Feedback.msg_warning
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then (spc () ++ Errors.print e) else mt ())
     | Defining_principle e ->
-	Pp.msg_warning
+	Feedback.msg_warning
 	  (str "Cannot define principle(s) for "++
 	     h 1 (pr_enum Libnames.pr_reference names) ++
 	     if do_observe () then Errors.print e else mt ())
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8a0a1a064..72205e2bb 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.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 (*let observennl strm =
   if do_observe ()
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 84a4d910e..0cacb003d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -267,12 +267,12 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      msg_warning
+      Feedback.msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
   with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      msg_warning
+      Feedback.msg_warning
 	(str "Cannot build inversion information (early)" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
 
@@ -292,12 +292,12 @@ let warning_error names e =
   in
   match e with
     | Building_graph e ->
-      Pp.msg_warning
+      Feedback.msg_warning
 	(str "Cannot define graph(s) for " ++
 	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	   e_explain e)
     | Defining_principle e ->
-      Pp.msg_warning
+      Feedback.msg_warning
 	(str "Cannot define principle(s) for "++
 	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	   e_explain e)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 72529fbbe..94530bfde 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -53,7 +53,7 @@ let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 
 (*let observennl strm =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c71d9a9ca..99a165044 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -504,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
   match c1 , c2 with
     | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
-        let _ = prstr "\nICI1!\n";Pp.flush_all() in
+        let _ = prstr "\nICI1!\n" in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
     | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
     | GLetIn(_,nme,bdy,trm) , _ ->
-        let _ = prstr "\nICI2!\n";Pp.flush_all() in
+        let _ = prstr "\nICI2!\n" in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
-        let _ = prstr "\nICI3!\n";Pp.flush_all() in
+        let _ = prstr "\nICI3!\n" in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
+    | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
 let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
@@ -527,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
         GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
     | GLetIn(_,nme,bdy,trm) , _ ->
-        let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
+      let _ = prstr "\nICI2 '!\n" in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
     | _, GLetIn(_,nme,bdy,trm) ->
-        let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
+        let _ = prstr "\nICI3 '!\n" in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
         GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
+    | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 10f08d3d1..80866e8b8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -214,17 +214,17 @@ let print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
       else
 	begin
-	  Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
+	  Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
 	end;
       (* print_debug_queue false e; *)
     end
 
 let observe strm =
   if do_observe ()
-  then Pp.msg_debug strm
+  then Feedback.msg_debug strm
   else ()
 
 
@@ -1537,7 +1537,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e when Errors.noncritical e ->
 	begin
 	  if do_observe ()
-	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
+	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly (Pp.str "Cannot create equation Lemma")
 	  ;
 	  true
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 0fcfbfc71..e4aa1448e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -961,7 +961,7 @@ struct
 
   let parse_expr parse_constant parse_exp ops_spec env term =
     if debug
-    then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
+    then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
 
 (*
     let constant_or_variable env term =
@@ -1082,7 +1082,7 @@ struct
 
   let rconstant term = 
     if debug
-    then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
+    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
     let res = rconstant term in
       if debug then 
 	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1122,7 +1122,7 @@ struct
 
   let  parse_arith parse_op parse_expr env cstr gl =
    if debug
-   then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm  cstr ++ fnl ());
+   then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm  cstr ++ fnl ());
    match kind_of_term cstr with
     | App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
@@ -1651,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
 
  if debug then
    begin
-     Pp.pp (Pp.str "Formula....\n") ;
+     Feedback.msg_notice (Pp.str "Formula....\n") ;
      let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
      let ff = dump_formula formula_typ
        (dump_cstr spec.typ spec.dump_coeff) ff in
-       Pp.pp (Printer.prterm ff) ;  Pp.pp_flush ();
-         Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+       Feedback.msg_notice (Printer.prterm ff);
+       Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
    end;
 
  match witness_list_tags prover cnf_ff with
@@ -1676,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
 
   if debug then
     begin
-      Pp.pp (Pp.str "\nAFormula\n") ;
+      Feedback.msg_notice (Pp.str "\nAFormula\n") ;
       let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
       let ff' = dump_formula formula_typ
         (dump_cstr spec.typ spec.dump_coeff) ff' in
-        Pp.pp (Printer.prterm  ff') ;  Pp.pp_flush ();
+        Feedback.msg_notice (Printer.prterm  ff');
         Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
     end;
 
@@ -1733,7 +1733,7 @@ let micromega_gen
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
     | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
-    | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+    | CsdpNotFound -> flush stdout ;
      Tacticals.New.tclFAIL 0 (Pp.str 
                            (" Skipping what remains of this tactic: the complexity of the goal requires "
                             ^ "the use of a specialized external tool called csdp. \n\n" 
@@ -1818,7 +1818,7 @@ let micromega_genr prover =
   with
   | Mfourier.TimeOut     -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
   | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
-  | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+  | CsdpNotFound ->
       Tacticals.New.tclFAIL 0 (Pp.str 
       (" Skipping what remains of this tactic: the complexity of the goal requires "
       ^ "the use of a specialized external tool called csdp. \n\n" 
@@ -1903,7 +1903,7 @@ let call_csdpcert_q provername poly =
      let cert = Certificate.q_cert_of_pos cert in
      if Mc.qWeakChecker poly cert
      then Some cert
-     else ((print_string "buggy certificate" ; flush stdout) ;None)
+     else ((print_string "buggy certificate") ;None)
 
 let call_csdpcert_z provername poly =
  let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index dca46cbcf..007a9ec67 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -172,7 +172,7 @@ let print_env_reification env =
   in
   let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
   let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
-  msg_debug (prop_info ++ fnl () ++ term_info)
+  Feedback.msg_debug (prop_info ++ fnl () ++ term_info)
 
 (* \subsection{Gestion des environnements de variable pour Omega} *)
 (* generation d'identifiant d'equation pour Omega *)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 3ba92b9f2..f3eae5f50 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -547,7 +547,7 @@ let pp_info () =
 	int s_info.created_branches ++ str " created" ++ fnl () ++
 	str "Hypotheses : " ++
 	int s_info.created_hyps ++ str " created" ++ fnl () in
-    msg_info
+    Feedback.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 73dc13e72..0a0b45915 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -276,7 +276,7 @@ let rtauto_tac gls=
     begin
       reset_info ();
       if !verbose then
-	msg_info (str "Starting proof-search ...");
+	Feedback.msg_info (str "Starting proof-search ...");
     end in
   let search_start_time = System.get_time () in
   let prf =
@@ -286,10 +286,10 @@ let rtauto_tac gls=
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
-      msg_info (str "Proof tree found in " ++
+      Feedback.msg_info (str "Proof tree found in " ++
 	     System.fmt_time_difference search_start_time search_end_time);
       pp_info ();
-      msg_info (str "Building proof term ... ")
+      Feedback.msg_info (str "Building proof term ... ")
     end in
   let build_start_time=System.get_time () in
   let _ = step_count := 0; node_count := 0 in
@@ -302,7 +302,7 @@ let rtauto_tac gls=
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
-      msg_info (str "Proof term built in " ++
+      Feedback.msg_info (str "Proof term built in " ++
 	     System.fmt_time_difference build_start_time build_end_time ++
 	     fnl () ++
 	     str "Proof size : " ++ int !step_count ++
@@ -319,9 +319,9 @@ let rtauto_tac gls=
       Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
   let tac_end_time = System.get_time () in
   let _ =
-    if !check then msg_info (str "Proof term type-checking is on");
+    if !check then Feedback.msg_info (str "Proof term type-checking is on");
     if !verbose then
-      msg_info (str "Internal tactic executed in " ++
+      Feedback.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/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index f5a734048..f64226e33 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -60,9 +60,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
       let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
       add_theory id (ic t) set k cst (pre,post) power sign div]
   | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following ring structures have been declared:");
+    Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
+      Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
           str"with carrier "++ pr_constr fi.ring_carrier++spc()++
           str"and equivalence relation "++ pr_constr fi.ring_req))
@@ -89,9 +89,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
     let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
 | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
-    msg_notice (strbrk "The following field structures have been declared:");
+    Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
-      msg_notice (hov 2
+      Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
           str"with carrier "++ pr_constr fi.field_carrier++spc()++
           str"and equivalence relation "++ pr_constr fi.field_req))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 271bf35a8..154ec6e1b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -527,7 +527,7 @@ let ring_equality env evd (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
-		    msg_info
+		    Feedback.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++
@@ -536,7 +536,7 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		  op_morph)
             | None ->
 		(Flags.if_verbose
-		    msg_info
+		    Feedback.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/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5f44904c3..fe9386039 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -25,7 +25,7 @@ let threshold = of_int 5000
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
       if less_than threshold n then
-	msg_warning
+	Feedback.msg_warning
 	  (strbrk "Stack overflow or segmentation fault happens when " ++
 	   strbrk "working with large numbers in nat (observed threshold " ++
 	   strbrk "may vary from 5000 to 70000 depending on your system " ++
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ece92b66b..55220f44c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && is_verbose () then
-    msg_warning (message_ambig !ambig_paths)
+    Feedback.msg_warning (message_ambig !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 4fb411202..129725c6d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -50,11 +50,11 @@ type bound_ident_map = Id.t Id.Map.t
 exception PatternMatchingFailure
 
 let warn_bound_meta name =
-  msg_warning (str "Collision between bound variable " ++ pr_id name ++
+  Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++
     str " and a metavariable of same name.")
 
 let warn_bound_bound name =
-  msg_warning (str "Collision between bound variables of name " ++ pr_id name)
+  Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name)
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c973e1cef..86921c49b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t =
         share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
-        if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
+        if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
         let c = detype flags avoid env sigma c in
         let t = detype flags avoid env sigma t in
         (List.rev l,c,t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 08973a05c..89cb723bc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -501,7 +501,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
+	     Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
 		 ++ fnl ()) in
   match (flex_kind_of_term (fst ts) env evd term1 sk1, 
 	 flex_kind_of_term (fst ts) env evd term2 sk2) with
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e3b6fb08a..04100c8a7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -336,8 +336,8 @@ let glob_visible_short_qualid c =
 
 let add_and_check_ident id set =
   if Id.Set.mem id set then
-    Pp.(msg_warning
-      (str "Collision between bound variables of name " ++ Id.print id));
+    Feedback.msg_warning
+      Pp.(str "Collision between bound variables of name " ++ Id.print id);
   Id.Set.add id set
 
 let bound_glob_vars =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8b061e3c2..5d36fc78e 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -184,7 +184,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
                   (match dest_recarg ra with
 	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
 	            | Imbr _  ->
-		        msg_warning (strbrk "Ignoring recursive call");
+		        Feedback.msg_warning (strbrk "Ignoring recursive call");
 		        (None,rest)
                     | _ -> (None, rest))
 	  in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 17bf28793..2a5e99965 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -389,16 +389,16 @@ let native_norm env sigma c ty =
   let code, upd = mk_norm_code penv sigma prefix c in
   match Nativelib.compile ml_filename code with
     | true, fn ->
-        if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ...");
+        if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
         let t0 = Sys.time () in
         Nativelib.call_linker ~fatal:true prefix fn (Some upd);
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         let res = nf_val env !Nativelib.rt1 ty in
         let t2 = Sys.time () in
         let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
-        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         res
     | _ -> anomaly (Pp.str "Compilation failure") 
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 827071054..d6305d81a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -348,7 +348,7 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Pp.msg_warning (strbrk "Cast not taken into account in constr pattern");
+      Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern");
       pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6499ddd53..bbb6a9266 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -216,7 +216,7 @@ let compute_canonical_projections (con,ind) =
                    if Flags.is_verbose () then
                      (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-		      msg_warning (strbrk "No global reference exists for projection value"
+		      Feedback.msg_warning (strbrk "No global reference exists for projection value"
                                    ++ Termops.print_constr t ++ strbrk " in instance "  
                                    ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
 		   l
@@ -250,7 +250,7 @@ let open_canonical_structure i (_,o) =
               and new_can_s = (Termops.print_constr s.o_DEF) in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
-              msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
+              Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
                              ++ strbrk " by " ++ prj ++ strbrk " in "
                              ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b6eb3a037..79cb7a2f6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -802,14 +802,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack as s) =
     let () = if !debug_RAKAM then
 	let open Pp in
-	pp (h 0 (str "<<" ++ Termops.print_constr x ++
+	Feedback.msg_notice
+             (h 0 (str "<<" ++ Termops.print_constr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
 		   str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
 		   str ">>") ++ fnl ())
     in
     let fold () =
       let () = if !debug_RAKAM then
-	  let open Pp in pp (str "<><><><><>" ++ fnl ()) in
+	  let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
       (s,cst_l)
     in
     match kind_of_term x with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a4a386530..cdd543d25 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -657,7 +657,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     and cN = Evarutil.whd_head_evar sigma curn in
     let () = 
       if !debug_unification then
-	msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN)
+	Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN)
     in 
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
@@ -1054,7 +1054,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
     
-  if !debug_unification then msg_debug (str "Starting unification");
+  if !debug_unification then Feedback.msg_debug (str "Starting unification");
   let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
   try
   let res = 
@@ -1075,10 +1075,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     let a = match res with 
     | Some sigma -> sigma, ms, es
     | None -> unirec_rec (env,0) cv_pb opt subst m n in
-    if !debug_unification then msg_debug (str "Leaving unification with success");
+    if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
     a
   with e ->
-    if !debug_unification then msg_debug (str "Leaving unification with failure");
+    if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
     raise e
 
 
diff --git a/printing/printer.ml b/printing/printer.ml
index cb075c64f..a43ccff46 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -551,7 +551,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
   (* Side effect! This has to be made more robust *)
   let () =
     match close_cmd with
-    | Some cmd -> msg_info cmd
+    | Some cmd -> Feedback.msg_info cmd
     | None -> ()
   in
   match goals with
@@ -629,12 +629,12 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
           begin match bgoals,shelf,given_up with
 	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
           | [] , [] , _ ->
-	     msg_info (str "No more subgoals, but there are some goals you gave up:");
+	     Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
 	     fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
             ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
-	    msg_info (str "All the remaining goals are on the shelf.");
+	    Feedback.msg_info (str "All the remaining goals are on the shelf.");
 	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
 	  | _ , _, _ ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5367a907e..45af036fb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -111,7 +111,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
     in
     (p,status)
   with
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 681a7fa1a..caa9b328a 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -128,7 +128,7 @@ let suggest_Proof_using name env vars ids_typ context_ids =
   if S.equal all_needed fwd_typ then valid (str "Type*");
   if S.equal all all_needed then valid(str "All");
   valid (pr_set false needed);
-  msg_info (
+  Feedback.msg_info (
     str"The proof of "++ str name ++ spc() ++
     str "should start with one of the following commands:"++spc()++
     v 0 (
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 2d886b8e1..13b5848a3 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -31,7 +31,7 @@ let cbv_vm env sigma c =
 
 let cbv_native env sigma c =
   if Coq_config.no_native_compiler then
-    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
     cbv_vm env sigma c
   else
     let ctyp = Retyping.get_type_of env sigma c in
@@ -221,7 +221,7 @@ let reduction_of_red_expr env =
      let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
      let () =
        if not (!simplIsCbn || List.is_empty f.rConst) then
-	 Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+	 Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 186525e15..23433692c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
-  Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls
+  Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
@@ -218,7 +218,8 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
-  pp (str (emacs_str "<infoH>")
+  Feedback.msg_notice
+    (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
       ++  (str (emacs_str "</infoH>")) ++ fnl());
   tclIDTAC goal;;
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index c7faef333..0ca4d6020 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -104,7 +104,8 @@ module Make(T : Task) = struct
       marshal_err ("unmarshal_more_data: "^s)
 
   let report_status ?(id = !Flags.async_proofs_worker_id) s =
-    Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+    let open Feedback in
+    feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
 
   module Worker = Spawn.Sync(struct end)
 
@@ -302,8 +303,8 @@ module Make(T : Task) = struct
   let main_loop () =
     let slave_feeder oc fb =
       Marshal.to_channel oc (RespFeedback fb) []; flush oc in
-    Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
-    Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
+    Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+    Feedback.set_logger Feedback.feedback_logger;
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index ce5ef0169..afbc407d8 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -150,7 +150,7 @@ let find_mutually_recursive_statements thms =
 	  assert (List.is_empty rest);
           (* One occ. of common coind ccls and no common inductive hyps *)
 	  if not (List.is_empty common_same_indhyp) then
-	    if_verbose msg_info (str "Assuming mutual coinductive statements.");
+	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
 	  flush_all ();
           indccl, true, []
       | [], _::_ ->
@@ -158,7 +158,7 @@ let find_mutually_recursive_statements thms =
           | ind :: _ ->
             if List.distinct_f ind_ord (List.map pi1 ind)
             then
-              if_verbose msg_info
+              if_verbose Feedback.msg_info
                 (strbrk
                    ("Coinductive statements do not follow the order of "^
                     "definition, assuming the proof to be by induction."));
@@ -306,7 +306,7 @@ let admit (id,k,e) pl hook () =
   let () = match k with
   | Global, _, _ -> ()
   | Local, _, _ | Discharge, _, _ ->
-    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+    Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
       str "declared as an axiom.")
   in
   let () = assumption_message id in
@@ -336,7 +336,7 @@ let universe_proof_terminator compute_guard hook =
   make_terminator begin function
   | Admitted (id,k,pe,(ctx,pl)) ->
       admit (id,k,pe) pl (hook (Some ctx)) ();
-      Pp.feedback Feedback.AddedAxiom
+      Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
         | Vernacexpr.Transparent -> false, true, []
diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b6..28e749d5c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -18,6 +18,7 @@ open Names
 open Util
 open Ppvernac
 open Vernac_classifier
+open Feedback
 
 module Hooks = struct
 
@@ -27,28 +28,23 @@ let with_fail, with_fail_hook = Hook.make ()
 
 let state_computed, state_computed_hook = Hook.make
  ~default:(fun state_id ~in_cache ->
-    feedback ~state_id Feedback.Processed) ()
+    feedback ~id:(State state_id) Processed) ()
 
 let state_ready, state_ready_hook = Hook.make
  ~default:(fun state_id -> ()) ()
 
 let forward_feedback, forward_feedback_hook = Hook.make
  ~default:(function
-    | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
-          feedback ~edit_id ~route contents
-    | { Feedback.id = Feedback.State state_id; route; contents } ->
-          feedback ~state_id ~route contents) ()
+    | { id = id; route; contents } ->
+      feedback ~id:id ~route contents) ()
 
 let parse_error, parse_error_hook = Hook.make
- ~default:(function
-    | Feedback.Edit edit_id -> fun loc msg ->
-        feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
-    | Feedback.State state_id -> fun loc msg ->
-        feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ ~default:(fun id loc msg ->
+        feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
 
 let execution_error, execution_error_hook = Hook.make
  ~default:(fun state_id loc msg ->
-    feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+    feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun _ _ -> ()) ()
@@ -106,11 +102,11 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
     | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
     | _ -> false in
   if internal_command expr then begin
-    prerr_endline (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr))
+    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
   end else begin
-    set_id_for_feedback ?route (Feedback.State id);
+    set_id_for_feedback ?route (State id);
     Aux_file.record_in_aux_set_at loc;
-    prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr));
+    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
     try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
     with e ->
       let e = Errors.push e in
@@ -120,8 +116,8 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
 (* Wrapper for Vernac.parse_sentence to set the feedback id *)
 let vernac_parse ?newtip ?route eid s =
   let feedback_id = 
-    if Option.is_empty newtip then Feedback.Edit eid
-    else Feedback.State (Option.get newtip) in
+    if Option.is_empty newtip then Edit eid
+    else State (Option.get newtip) in
   set_id_for_feedback ?route feedback_id;
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   Flags.with_option Flags.we_are_parsing (fun () ->
@@ -138,7 +134,7 @@ let vernac_parse ?newtip ?route eid s =
 
 let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
-  with Proof_global.NoCurrentProof -> str""
+  with Proof_global.NoCurrentProof -> Pp.str ""
 
 let update_global_env () =
   if Proof_global.there_are_pending_proofs () then
@@ -230,7 +226,7 @@ end = struct (* {{{ *)
   let find_proof_at_depth vcs pl =
     try List.find (function
           | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
-          | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
           | _ -> false)
         (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
     with Not_found -> failwith "find_proof_at_depth"
@@ -238,9 +234,9 @@ end = struct (* {{{ *)
   exception Expired
   let visit vcs id =
     if Stateid.equal id Stateid.initial then
-      anomaly(str"Visiting the initial state id")
+      anomaly(Pp.str "Visiting the initial state id")
     else if Stateid.equal id Stateid.dummy then
-      anomaly(str"Visiting the dummy state id")
+      anomaly(Pp.str "Visiting the dummy state id")
     else
     try
       match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -256,7 +252,7 @@ end = struct (* {{{ *)
       | [n, Sideff (Some x); p, Noop]
       | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
       | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
-      | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
+      | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
 end (* }}} *)
@@ -339,10 +335,10 @@ end = struct (* {{{ *)
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
     let string_of_transaction = function
       | Cmd { cast = t } | Fork (t, _,_,_) ->
-          (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+          (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff (Some t) ->
           sprintf "Sideff(%s)"
-            (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+            (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff None -> "EnvChange"
       | Noop -> " "
       | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
@@ -740,7 +736,7 @@ end = struct (* {{{ *)
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
   =
-    feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+    feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
     let str_id = Stateid.to_string id in
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
@@ -1062,7 +1058,7 @@ end = struct (* {{{ *)
         List.iter (fun (id,s) -> State.assign id s) l; `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
               RespBuiltProof (pl, time) ->
-        feedback (Feedback.InProgress ~-1);
+        feedback (InProgress ~-1);
         t_assign (`Val pl);
         record_pb_time t_name t_loc time;
         if !Flags.async_proofs_full || t_drop
@@ -1070,7 +1066,7 @@ end = struct (* {{{ *)
         else `End
     | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
             RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
-        feedback (Feedback.InProgress ~-1);
+        feedback (InProgress ~-1);
         let info = Stateid.add ~valid Exninfo.null e_error_at in
         let e = (RemoteException e_msg, info) in
         t_assign (`Exn e);
@@ -1086,7 +1082,7 @@ end = struct (* {{{ *)
         let e = (RemoteException (strbrk s), info) in
         t_assign (`Exn e);
         Hooks.(call execution_error start Loc.ghost (strbrk s));
-        feedback (Feedback.InProgress ~-1)
+        feedback (InProgress ~-1)
 
   let build_proof_here ~drop_pt (id,valid) loc eop =
     Future.create (State.exn_on id ~valid) (fun () ->
@@ -1097,7 +1093,7 @@ end = struct (* {{{ *)
       Aux_file.record_in_aux_at loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       let p = Proof_global.return_proof ~allow_partial:drop_pt () in
-      if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+      if drop_pt then feedback ~id:(State id) Complete;
       p)
 
   let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1190,7 +1186,7 @@ end = struct (* {{{ *)
         "The system state could not be sent to the worker process. "^
         "Falling back to local, lazy, evaluation."));
       t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
-      feedback (Feedback.InProgress ~-1)
+      feedback (InProgress ~-1)
 
 end (* }}} *)
 
@@ -1270,7 +1266,7 @@ end = struct (* {{{ *)
       let (e, info) = Errors.push e in
       (try match Stateid.get info with
       | None ->
-          pperrnl (
+          msg_error (
             str"File " ++ str name ++ str ": proof of " ++ str r_name ++
             spc () ++ iprint (e, info))
       | Some (_, cur) ->
@@ -1280,12 +1276,12 @@ end = struct (* {{{ *)
           | { step = `Qed ( { qast = { loc } }, _) } 
           | { step = `Sideff (`Ast ( { loc }, _)) } ->
               let start, stop = Loc.unloc loc in
-              pperrnl (
+              msg_error (
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 str ": chars " ++ int start ++ str "-" ++ int stop ++
                 spc () ++ iprint (e, info))
           | _ ->
-              pperrnl (
+              msg_error (
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
                 spc () ++ iprint (e, info))
     with e ->
@@ -1378,7 +1374,7 @@ end = struct (* {{{ *)
     else 
       let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
-      feedback (Feedback.InProgress 1);
+      feedback (InProgress 1);
       let task = ProofTask.(BuildProof {
         t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
         t_loc = loc; t_uuid; t_name = pname;
@@ -1625,11 +1621,11 @@ end = struct (* {{{ *)
     Reach.known_state ~cache:`No r_where;
     try
       vernac_interp r_for { r_what with verbose = true };
-      feedback ~state_id:r_for Feedback.Processed     
+      feedback ~id:(State r_for) Processed
     with e when Errors.noncritical e ->
       let e = Errors.push e in
       let msg = string_of_ppcmds (iprint e) in
-      feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+      feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1897,7 +1893,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     vernac_interp id ~proof x;
-                    feedback ~state_id:id Feedback.Incomplete
+                    feedback ~id:(State id) Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
                 Proof_global.discard_all ()
@@ -2034,7 +2030,6 @@ let check_task name (tasks,rcbackup) i =
   let vcs = VCS.backup () in
   try
     let rc = Future.purify (Slaves.check_task name tasks) i in
-    pperr_flush ();
     VCS.restore vcs;
     rc
   with e when Errors.noncritical e -> VCS.restore vcs; false
@@ -2044,7 +2039,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
   let finish_task u (_,_,i) =
     let vcs = VCS.backup () in
     let u = Future.purify (Slaves.finish_task name u d p t) i in
-    pperr_flush ();
     VCS.restore vcs;
     u in
   try
@@ -2052,7 +2046,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
     (u,a,true), p
   with e ->
     let e = Errors.push e in
-    pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+    msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
     exit 1
 
 let merge_proof_branch ?valid ?id qast keep brname =
@@ -2357,7 +2351,7 @@ type focus = {
   tip : Stateid.t
 }
 
-let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
   Future.purify (fun s ->
     if Stateid.equal at Stateid.dummy then finish ()
     else Reach.known_state ~cache:`Yes at;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6b58baa99..e57b48e9e 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 cfbcc4750..95b26c2d5 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 f0f408c24..2cae9b794 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 b2104ba43..b543b564c 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 15e9d3a94..a2431f6ef 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 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 13705edaa..9886b263c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -502,7 +502,7 @@ let coqdep () =
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
-      (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -527,4 +527,4 @@ let _ =
     coqdep ()
   with Errors.UserError(s,p) ->
     let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
-    Pp.msgerrnl pp
+    Feedback.msg_error pp
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index e81f4038d..d5ef807b6 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -36,10 +36,10 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    if Pp.is_message xml then
-      let message = Pp.to_message xml in
-      let level = message.Pp.message_level in
-      let content = message.Pp.message_content in
+    if Feedback.is_message xml then
+      let message = Feedback.to_message xml in
+      let level = message.Feedback.message_level in
+      let content = message.Feedback.message_content in
       logger level content;
       loop ()
     else if Feedback.is_feedback xml then
diff --git a/toplevel/class.ml b/toplevel/class.ml
index a9c53b4d4..10e9b30be 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -262,7 +262,7 @@ let add_new_coercion_core coef stre poly source target isid =
   in
   check_source (Some cls);
   if not (uniform_cond (llp-ind) lvs) then
-    msg_warning (explain_coercion_error coef NotUniform);
+    Feedback.msg_warning (explain_coercion_error coef NotUniform);
   let clt =
     try
       get_target tg ind
@@ -310,7 +310,7 @@ let add_coercion_hook poly local ref =
   in
   let () = try_add_new_coercion ref stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
-  Flags.if_verbose msg_info msg
+  Flags.if_verbose Feedback.msg_info msg
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5865fec06..f0f678e08 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -119,7 +119,7 @@ let interp_definition pl bl p red_option c ctypopt =
           impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
-	then msg_warning
+	then Feedback.msg_warning
           (strbrk "Implicit arguments declaration relies on type." ++ spc () ++
 	   strbrk "The term declares more implicits than the type here.");
         let vars = Univ.LSet.union (Universes.universes_of_constr body) 
@@ -140,7 +140,7 @@ let get_locality id = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
   let msg = pr_id id ++ strbrk " is declared as a local definition" in
-  let () = msg_warning msg in
+  let () = Feedback.msg_warning msg in
   true
 | Local -> true
 | Global -> false
@@ -171,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = if Pfedit.refining () then
       let msg = strbrk "Section definition " ++
         pr_id ident ++ strbrk " is not visible from current goals" in
-      msg_warning msg
+      Feedback.msg_warning msg
     in
     gr
   | Discharge | Local | Global ->
@@ -217,7 +217,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if is_verbose () && Pfedit.refining () then
-    msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+    Feedback.msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
   let r = VarRef ident in
@@ -706,7 +706,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 		constrimpls)
       impls;
   let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
-  if_verbose msg_info (minductive_message warn_prim names);
+  if_verbose Feedback.msg_info (minductive_message warn_prim names);
   if mie.mind_entry_private == None
   then declare_default_schemes mind;
   mind
@@ -799,7 +799,7 @@ let check_mutuality env isfix fixl =
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
-	msg_warning (non_full_mutual_message x xge y yge isfix rest)
+	Feedback.msg_warning (non_full_mutual_message x xge y yge isfix rest)
     | _ -> ()
 
 type structured_fixpoint_expr = {
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b81c8da71..e4975fa31 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -36,7 +36,7 @@ let load_rcfile() =
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
-	  let warn x = msg_warning (str x) in
+	  let warn x = Feedback.msg_warning (str x) in
 	  let inferedrc = List.find CUnix.file_readable_p [
 	    Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
 	    Envars.xdg_config_home warn / rcdefaultname;
@@ -52,10 +52,10 @@ let load_rcfile() =
 	*)
     with reraise ->
       let reraise = Errors.push reraise in
-      let () = msg_info (str"Load of rcfile failed.") in
+      let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
   else
-    Flags.if_verbose msg_info (str"Skipping rcfile loading.")
+    Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.")
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
@@ -78,7 +78,7 @@ let push_ml_include s = ml_includes := s :: !ml_includes
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
+  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
   let coqpath = Envars.coqpath in
   let coq_root = Names.DirPath.make [Nameops.coq_root] in
     (* NOTE: These directories are searched from last to first *)
@@ -135,6 +135,6 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
+    Feedback.msg_warning (str "Compatibility with version " ++ str s ++ str " not supported.");
     Flags.V8_2
   | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 040c33924..c8879963e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,6 +13,8 @@ open Flags
 open Vernac
 open Pcoq
 
+let top_stderr x = msg_with !Pp_control.err_ft x
+
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
@@ -59,7 +61,7 @@ let prompt_char ic ibuf count =
     | ll::_ -> Int.equal ibuf.len ll
     | [] -> Int.equal ibuf.len 0
   in
-  if bol && not !print_emacs then msgerr (str (ibuf.prompt()));
+  if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -310,23 +312,23 @@ let read_sentence () =
 *)
 
 let do_vernac () =
-  msgerrnl (mt ());
-  if !print_emacs then msgerr (str (top_buffer.prompt()));
+  top_stderr (fnl());
+  if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
     Vernac.eval_expr (read_sentence ())
   with
     | End_of_input | Errors.Quit ->
-        msgerrnl (mt ()); pp_flush(); raise Errors.Quit
+        top_stderr (fnl ()); raise Errors.Quit
     | Errors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise Errors.Drop
-        else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
+        else Feedback.msg_error (str"There is no ML toplevel.")
     | any ->
         let any = Errors.push any in
         Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
-        pp_flush ()
+        flush_all ()
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -354,7 +356,7 @@ let rec loop () =
     | Errors.Drop -> ()
     | Errors.Quit -> exit 0
     | any ->
-      msgerrnl (str"Anomaly: main loop exited with exception: " ++
+      Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
                 str (Printexc.to_string any) ++
                 fnl() ++ str"Please report.");
       loop ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4222b330..869f6bb93 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -31,10 +31,10 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = get_version_date () in
-  ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
-  pp_flush ()
+  Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+  flush_all ()
 
-let warning s = with_option Flags.warn msg_warning (strbrk s)
+let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
 
 let toploop = ref None
 
@@ -61,7 +61,8 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Ppstyle.init_color_output ()
+      Ppstyle.init_color_output ();
+      Feedback.set_logger Feedback.color_terminal_logger
     | Some "" ->
       (** No color output *)
       ()
@@ -69,7 +70,8 @@ let init_color () =
       (** Overwrite all colors *)
       Ppstyle.clear_styles ();
       Ppstyle.parse_config s;
-      Ppstyle.init_color_output ()
+      Ppstyle.init_color_output ();
+      Feedback.set_logger Feedback.color_terminal_logger
   end
 
 let toploop_init = ref begin fun x ->
@@ -95,8 +97,8 @@ let memory_stat = ref false
 let print_memory_stat () =
   begin (* -m|--memory from the command-line *)
     if !memory_stat then
-    ppnl
-      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes");
+    Feedback.msg_notice
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ());
   end;
   begin
     (* operf-macro interface:
@@ -141,7 +143,7 @@ let remove_top_ml () = Mltop.remove ()
 
 let inputstate = ref ""
 let set_inputstate s =
-  let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
+  let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
 let inputstate () =
   if not (String.is_empty !inputstate) then
@@ -150,7 +152,7 @@ let inputstate () =
 
 let outputstate = ref ""
 let set_outputstate s =
-  let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
+  let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
 let outputstate () =
   if not (String.is_empty !outputstate) then
@@ -243,7 +245,7 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
-  Pp.make_pp_emacs ();
+  Feedback.(set_logger emacs_logger);
   Vernacentries.qed_display_script := false;
   color := `OFF
 
@@ -646,7 +648,7 @@ let init_toplevel arglist =
   if !batch_mode then begin
     flush_all();
     if !output_context then
-      Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+      Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
   end
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 367425546..f995a390c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
   | UserAutomaticRequest
   | InternalTacticRequest ->
     (if debug then
-      msg_warning
+      Feedback.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
   | _ -> Some msg
 
@@ -303,7 +303,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
-      msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
+      Feedback.msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
   end
 
 let declare_sym_scheme ind =
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index ef789aa5c..c4c891b89 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -35,7 +35,7 @@ let enforce_locality_full locality_flag local =
 	Errors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
-          Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
+          Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
 	  Some true
 	end else
 	None
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d60c73939..52117f13f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -568,7 +568,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 ->
-      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+      Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       CLexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -577,7 +577,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+      Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       CLexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -855,12 +855,12 @@ let check_rule_productivity l =
 let is_not_printable onlyparse noninjective = function
 | NVar _ ->
   let () = if not onlyparse then
-    msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
+    Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
   in
   true
 | _ ->
   if not onlyparse && noninjective then
-    let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+    let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
     true
   else onlyparse
 
@@ -886,7 +886,7 @@ let find_precedence lev etyps symbols =
 	| ETName | ETBigint | ETReference ->
             begin match lev with
             | None ->
-	      ([msg_info,strbrk "Setting notation at level 0."],0)
+	      ([Feedback.msg_info,strbrk "Setting notation at level 0."],0)
             | Some 0 ->
               ([],0)
             | _ ->
@@ -904,7 +904,7 @@ let find_precedence lev etyps symbols =
 	else [],Option.get lev)
   | Terminal _ when last_is_terminal () ->
       if Option.is_empty lev then
-	([msg_info,strbrk "Setting notation at level 0."], 0)
+	([Feedback.msg_info,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
   | _ ->
       if Option.is_empty lev then error "Cannot determine the level.";
@@ -931,7 +931,7 @@ let remove_curly_brackets l =
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
                   if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
-                    msg_warning (strbrk "Skipping spaces inside curly brackets");
+                    Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets");
                   if deb && List.is_empty l'' then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
@@ -976,7 +976,7 @@ let compute_pure_syntax_data df mods =
   let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
   let msgs =
     if onlyparse then
-      (msg_warning,
+      (Feedback.msg_warning,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
   msgs, sy_data, extra
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index d0fa7a80c..36c16208c 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -146,7 +146,7 @@ let dir_ml_load s =
 let dir_ml_use s =
   match !load with
     | WithTop t -> t.use_file s
-    | _ -> msg_warning (str "Cannot access the ML compiler")
+    | _ -> Feedback.msg_warning (str "Cannot access the ML compiler")
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
@@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path =
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
+    Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
 let add_rec_path ~unix_path ~coq_root ~implicit =
@@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let () = List.iter add dirs in
     Loadpath.add_load_path unix_path ~implicit coq_root
   else
-    msg_warning (str "Cannot open " ++ str unix_path)
+    Feedback.msg_warning (str "Cannot open " ++ str unix_path)
 
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
@@ -324,10 +324,10 @@ let if_verbose_load verb f name ?path fname =
     let info = str "[Loading ML file " ++ str fname ++ str " ..." in
     try
       let path = f name ?path fname in
-      msg_info (info ++ str " done]");
+      Feedback.msg_info (info ++ str " done]");
       path
     with reraise ->
-      msg_info (info ++ str " failed]");
+      Feedback.msg_info (info ++ str " failed]");
       raise reraise
 
 (** Load a module for the first time (i.e. dynlink it)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 54baa5e3c..dbc3ccaac 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -24,7 +24,7 @@ let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
 let trace s =
-  if !Flags.debug then msg_debug s
+  if !Flags.debug then Feedback.msg_debug s
   else ()
 
 let succfix (depth, fixrels) =
@@ -731,11 +731,11 @@ type progress =
 let obligations_message rem =
   if rem > 0 then
     if Int.equal rem 1 then
-      Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
     else
-      Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
+      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
   else
-    Flags.if_verbose msg_info (str "No more obligations remaining")
+    Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
 
 let update_obls prg obls rem =
   let prg' = { prg with prg_obligations = (obls, rem) } in
@@ -992,7 +992,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 msg_info (str "Solving obligations automatically...");
+  Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically...");
   try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
 
 open Pp
@@ -1000,13 +1000,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 msg_info (int rem ++ str " obligation(s) remaining: ");
+    if msg then Feedback.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;
-			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
 				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
 					    str "." ++ fnl ())))
@@ -1035,12 +1035,12 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
   let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
-    Flags.if_verbose msg_info (info ++ str ".");
+    Flags.if_verbose Feedback.msg_info (info ++ str ".");
     let cst = declare_definition prg in
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d12b5ee8e..0c3bd953c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -196,7 +196,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then errorlabstrm "structure" st;
-  Flags.if_verbose msg_warning (hov 0 st)
+  Flags.if_verbose Feedback.msg_warning (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	| Some None | None -> false
       in
 	if not is_primitive then 
-	  Flags.if_verbose msg_warning
+	  Flags.if_verbose Feedback.msg_warning
 	    (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
 		      str" could not be defined as a primitive record"));
 	is_primitive
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64225a644..1c3f0d997 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,8 +119,7 @@ let verbose_phrase verbch loc =
 	let s = String.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
-        ppnl (str s);
-        pp_flush()
+        Feedback.msg_notice (str s ++ fnl ())
     | None -> ()
 
 exception End_of_input
@@ -152,9 +151,9 @@ let pr_new_syntax loc ocom =
     | Some com -> Ppvernac.pr_vernac com
     | None -> mt() in
   if !beautify_file then
-    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    Feedback.msg_notice (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
-    msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+    Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
@@ -193,14 +192,15 @@ let display_cmd_header loc com =
     with e -> str (Printexc.to_string e) in
   let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
   in
-  Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
-	 str " [" ++ str cmd ++ str "] ");
-  Pp.flush_all ()
+  Feedback.msg_notice
+    (str "Chars " ++ int start ++ str " - " ++ int stop ++
+     str " [" ++ str cmd ++ str "] ")
+
 
 let rec vernac_com verbose checknav (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
-	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
 	let st = save_translator_coqdoc () in
@@ -248,8 +248,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc_ast = parse_sentence input in
-      vernac_com verbosely checknav loc_ast;
-      pp_flush ()
+      vernac_com verbosely checknav loc_ast
     done
   with any ->   (* whatever the exception *)
     let (e, info) = Errors.push any in
@@ -294,7 +293,7 @@ let load_vernac verb file =
 let ensure_v f =
   if Filename.check_suffix f ".v" then f
   else begin
-    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
     expanded to \"" ++ str f ++ str ".v\"");
     f ^ ".v"
   end
@@ -304,7 +303,7 @@ let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
     if not (List.is_empty pfs) then
-      (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 23755dac1..222b7d3df 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -57,7 +57,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
-  msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+  Feedback.msg_notice (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, 
@@ -65,22 +65,22 @@ let show_node () =
   ()
 
 let show_thesis () =
-     msg_error (anomaly (Pp.str "TODO") )
+     Feedback.msg_error (anomaly (Pp.str "TODO") )
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = get_pftreestate () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
-  msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
+  Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
 
 let show_universes () =
   let pfts = get_pftreestate () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
-    msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
-    msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
+    Feedback.msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma));
+    Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx)
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
@@ -91,11 +91,10 @@ let enable_goal_printing = ref true
 let print_subgoals () =
   if !enable_goal_printing && is_verbose ()
   then begin
-    msg_notice (pr_open_subgoals ())
+    Feedback.msg_notice (pr_open_subgoals ())
   end
 
 let try_print_subgoals () =
-  Pp.flush_all();
   try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
 
 
@@ -109,10 +108,10 @@ let show_intro all =
     let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
     if all then
       let lid = Tactics.find_intro_names l gl in
-      msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
+      Feedback.msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
     else if not (List.is_empty l) then
       let n = List.last l in
-      msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+      Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
   end
 
 (** Prepare a "match" template for a given inductive type.
@@ -153,7 +152,7 @@ let show_match id =
   let pr_branch l =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
   in
-  msg_notice (v 1 (str "match # with" ++ fnl () ++
+  Feedback.msg_notice (v 1 (str "match # with" ++ fnl () ++
 	    prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()))
 
 (* "Print" commands *)
@@ -194,23 +193,23 @@ let print_module r =
     let globdir = Nametab.locate_dir qid in
       match globdir with
 	  DirModule (dirpath,(mp,_)) ->
-	    msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
+	    Feedback.msg_notice (Printmod.print_module (Printmod.printable_body dirpath) mp)
 	| _ -> raise Not_found
   with
-      Not_found -> msg_error (str"Unknown Module " ++ pr_qualid qid)
+      Not_found -> Feedback.msg_error (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
-    msg_notice (Printmod.print_modtype kn)
+    Feedback.msg_notice (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
-      msg_notice (Printmod.print_module false mp)
+      Feedback.msg_notice (Printmod.print_module false mp)
     with Not_found ->
-      msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
+      Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let print_namespace ns =
   let ns = List.rev (Names.DirPath.repr ns) in
@@ -279,7 +278,7 @@ let print_namespace ns =
         acc
     ) constants (str"")
   in
-  msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
+  Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
 
 let print_strategy r =
   let open Conv_oracle in
@@ -309,7 +308,7 @@ let print_strategy r =
       else str "Constant strategies" ++ fnl () ++
         hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
     in
-    msg_notice (var_msg ++ cst_msg)
+    Feedback.msg_notice (var_msg ++ cst_msg)
   | Some r ->
     let r = Smartlocate.smart_global r in
     let key = match r with
@@ -318,7 +317,7 @@ let print_strategy r =
     | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
     in
     let lvl = get_strategy oracle key in
-    msg_notice (pr_strategy (r, lvl))
+    Feedback.msg_notice (pr_strategy (r, lvl))
 
 let dump_universes_gen g s =
   let output = open_out s in
@@ -352,7 +351,7 @@ let dump_universes_gen g s =
   try
     UGraph.dump_universes output_constraint g;
     close ();
-    msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
+    Feedback.msg_info (str "Universes written to file \"" ++ str s ++ str "\".")
   with reraise ->
     let reraise = Errors.push reraise in
     close ();
@@ -367,11 +366,11 @@ let locate_file f =
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->
-      msg_info (hov 0
+      Feedback.msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
 	 str file))
   | Library.LibInPath, fulldir, file ->
-      msg_info (hov 0
+      Feedback.msg_info (hov 0
 	(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
 
 let err_unmapped_library loc ?from qid =
@@ -506,7 +505,7 @@ let vernac_exact_proof c =
      called only at the begining of a proof. *)
   let status = by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
-  if not status then Pp.feedback Feedback.AddedAxiom
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption locality poly (local, kind) l nl =
   let local = enforce_locality_exp locality local in
@@ -518,7 +517,7 @@ let vernac_assumption locality poly (local, kind) l nl =
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
-  if not status then Pp.feedback Feedback.AddedAxiom
+  if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_record k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
@@ -636,7 +635,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 msg_info (str "Module " ++ pr_id id ++ str " is declared");
+  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -657,7 +656,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
            export id binders_ast mty_ast_o
        in
        Dumpglob.dump_moddef loc mp "mod";
-       if_verbose msg_info
+       if_verbose Feedback.msg_info
          (str "Interactive Module " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -675,7 +674,7 @@ 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 msg_info
+       if_verbose Feedback.msg_info
 	 (str "Module " ++ pr_id id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
          export
@@ -683,7 +682,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined");
+  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " 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 =
@@ -704,7 +703,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
            id binders_ast mty_sign
        in
        Dumpglob.dump_moddef loc mp "modtype";
-       if_verbose msg_info
+       if_verbose Feedback.msg_info
 	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -723,13 +722,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	    id binders_ast mty_sign mty_ast_l
         in
         Dumpglob.dump_moddef loc mp "modtype";
-	if_verbose msg_info
+	if_verbose Feedback.msg_info
 	  (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+  if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -797,7 +796,7 @@ let vernac_coercion locality poly local ref qids qidt =
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
   Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
-  if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
+  if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion locality poly local id qids qidt =
   let local = enforce_locality locality local in
@@ -813,7 +812,7 @@ let vernac_instance abst locality poly sup inst props pri =
   ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
 let vernac_context poly l =
-  if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom
+  if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
@@ -869,7 +868,7 @@ let vernac_set_used_variables e =
 (* Auxiliary file management *)
 
 let expand filename =
-  Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
+  Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
 let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
@@ -889,13 +888,13 @@ let vernac_declare_ml_module locality l =
   Mltop.declare_ml_modules local (List.map expand l)
 
 let vernac_chdir = function
-  | None -> msg_notice (str (Sys.getcwd()))
+  | None -> Feedback.msg_notice (str (Sys.getcwd()))
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err -> msg_warning (str "Cd failed: " ++ str err)
+	with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err)
       end;
-      if_verbose msg_info (str (Sys.getcwd()))
+      if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
 
 (********************)
@@ -1068,7 +1067,7 @@ let vernac_declare_arguments locality r l nargs flags =
           some_scopes_specified ||
           some_simpl_flags_specified) &&
      no_flags then
-    msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
+    Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'")
 
 
 let default_env () = {
@@ -1423,7 +1422,7 @@ let vernac_check_may_eval redexp glopt rc =
     | None ->
         let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
-	msg_notice (print_judgment env sigma' j ++
+	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
@@ -1434,7 +1433,7 @@ let vernac_check_may_eval redexp glopt rc =
           let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
           c
         in
-	msg_notice (print_eval redfun env sigma' rc j)
+	Feedback.msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
@@ -1450,7 +1449,7 @@ let vernac_global_check c =
   let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
-    msg_notice (print_safe_judgment env sigma j)
+    Feedback.msg_notice (print_safe_judgment env sigma j)
 
 
 let get_nth_goal n =
@@ -1487,7 +1486,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
     | NoHyp | Not_found -> print_about ref_or_by_not
 
 	       
-let vernac_print = function
+let vernac_print = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
   | PrintFullContext-> msg_notice (print_full_context_typ ())
   | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1586,6 +1585,7 @@ let vernac_search s gopt r =
     | Some g -> snd (Pfedit.get_goal_context g) , Some g
   in
   let get_pattern c = snd (intern_constr_pattern env c) in
+  let open Feedback in
   match s with
   | SearchPattern c ->
       msg_notice (Search.search_pattern gopt (get_pattern c) r)
@@ -1596,8 +1596,8 @@ let vernac_search s gopt r =
   | SearchAbout sl ->
      msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r)
 
-let vernac_locate = function
-  | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
+let vernac_locate = let open Feedback in function
+  | LocateAny (AN qid)  -> msg_notice (print_located_qualid qid)
   | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
   | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
   | LocateTerm (ByNotation (_, ntn, sc)) ->
@@ -1640,7 +1640,7 @@ let vernac_unfocus () =
 let vernac_unfocused () =
   let p = Proof_global.give_me_the_proof () in
   if Proof.unfocused p then
-    msg_notice (str"The proof is indeed fully unfocused.")
+    Feedback.msg_notice (str"The proof is indeed fully unfocused.")
   else
     error "The proof is not fully unfocused."
 
@@ -1668,7 +1668,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
   Proof_global.simple_with_current_proof (fun _ p ->
     Proof_global.Bullet.put p bullet)
 
-let vernac_show = function
+let vernac_show = let open Feedback in function
   | ShowGoal goalref ->
     let info = match goalref with
       | OpenSubgoals -> pr_open_subgoals ()
@@ -1706,7 +1706,7 @@ let vernac_check_guard () =
     with UserError(_,s) ->
       (str ("Condition violated: ") ++s)
   in
-  msg_notice message
+  Feedback.msg_notice message
 
 exception End_of_input
 
@@ -1717,7 +1717,7 @@ let vernac_load interp fname =
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
-    Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
+    Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in
   let input =
     let longfname = Loadpath.locate_file fname in
@@ -1849,15 +1849,15 @@ let interp ?proof ~loc locality poly c =
   | VernacSearch (s,g,r) -> vernac_search s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
-  | VernacComments l -> if_verbose msg_info (str "Comments ok\n")
+  | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> msg_warning (str "VernacAbort not handled by Stm")
-  | VernacAbortAll -> msg_warning (str "VernacAbortAll not handled by Stm")
-  | VernacRestart -> msg_warning (str "VernacRestart not handled by Stm")
-  | VernacUndo _ -> msg_warning (str "VernacUndo not handled by Stm")
-  | VernacUndoTo _ -> msg_warning (str "VernacUndoTo not handled by Stm")
-  | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm")
+  | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm")
+  | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm")
+  | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm")
+  | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm")
+  | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm")
+  | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm")
   
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -1991,7 +1991,7 @@ let with_fail b f =
       | HasNotFailed ->
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if is_verbose () || !test_mode || !ide_slave then msg_info
+          if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end
@@ -2016,7 +2016,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
     | VernacRedirect (s, (_,v)) ->
-         Pp.with_output_to_file s (aux false) v
+         Feedback.with_output_to_file s (aux false) v
     | VernacTime (_,v) ->
         System.with_time !Flags.time
           (aux ?locality ?polymorphism isprogcmd) v;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 7fbd2b119..1116a3104 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -55,7 +55,7 @@ let call ?locality (opn,converted_args) =
       | Egramml.GramNonTerminal _ -> str "_"
       in
       let pr = pr_sequence pr_gram rules in
-      msg_warning (str "Deprecated vernacular command: " ++ pr)
+      Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr)
     in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
@@ -68,5 +68,5 @@ let call ?locality (opn,converted_args) =
     | reraise ->
         let reraise = Errors.push reraise in
         if !Flags.debug then
-	  msg_debug (str"Vernac Interpreter " ++ str !loc);
+	  Feedback.msg_debug (str"Vernac Interpreter " ++ str !loc);
         iraise reraise