Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

82 files changed, 484 insertions, 879 deletions

diff --git a/Makefile.build b/Makefile.build
index 7dff7f2fce..e53ebf2e69 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -388,9 +388,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo)
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/cWarnings.cmo lib/minisys.cmo \
-  lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \
-  tools/coqdep.cmo
+COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/minisys.cmo lib/system.cmo \
+  tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
 
 $(COQDEP): $(call bestobj, $(COQDEPCMO))
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/checker/check.mllib b/checker/check.mllib
index 1925477e00..2fa4d57977 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -35,7 +35,6 @@ Segmenttree
 Unicodetable
 Unicode
 Errors
-CWarnings
 CEphemeron
 Future
 CUnix
diff --git a/dev/printers.mllib b/dev/printers.mllib
index e15855ef26..e39b780723 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -38,7 +38,6 @@ Segmenttree
 Unicodetable
 Unicode
 Errors
-CWarnings
 Bigint
 CUnix
 Minisys
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 2ec6430fdd..ac6a7ac7f2 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -111,8 +111,14 @@ let declare_tactic loc s c cl = match cl with
   declare_str_items loc
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac True False $name$ $body$ in
-      Tacenv.register_ml_tactic $se$ [|$tac$|];
-      Mltop.declare_cache_obj obj $plugin_name$; } >>
+      try do {
+        Tacenv.register_ml_tactic $se$ [|$tac$|];
+        Mltop.declare_cache_obj obj $plugin_name$; }
+      with [ e when Errors.noncritical e ->
+        Feedback.msg_warning
+          (Pp.app
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+            (Errors.print e)) ]; } >>
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
@@ -123,8 +129,14 @@ let declare_tactic loc s c cl = match cl with
   let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
+      try do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
+        Mltop.declare_cache_obj $obj$ $plugin_name$; }
+      with [ e when Errors.noncritical e ->
+        Feedback.msg_warning
+          (Pp.app
+            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
+            (Errors.print e)) ]; } >>
     ]
 
 open Pcaml
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 04b117fbad..ce04318894 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -122,8 +122,14 @@ let declare_command loc s c nt cl =
   let classl = make_fun_classifiers loc s c cl in
   declare_str_items loc
     [ <:str_item< do {
-        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$;
+	try do {
+          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 ->
+	  Feedback.msg_warning
+	    (Pp.app
+	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
+	       (Errors.print e)) ];
 	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
       } >> ]
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 18557ab6b4..f0e767cba3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -14,17 +14,15 @@ open Feedback
 
 let b2c = byte_offset_to_char_offset
 
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ]
-type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ]
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ]
+type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
 let mem_flag_of_flag : flag -> mem_flag = function
   | `ERROR _ -> `ERROR
-  | `WARNING _ -> `WARNING
   | (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
 let str_of_flag = function
   | `UNSAFE -> "U"
   | `PROCESSING -> "P"
   | `ERROR _ -> "E"
-  | `WARNING _ -> "W"
   | `INCOMPLETE -> "I"
 
 class type signals =
@@ -472,13 +470,6 @@ object(self)
           self#attach_tooltip sentence loc msg;
           if not (Loc.is_ghost loc) then
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
-      | Message(Warning, loc, msg), Some (id,sentence) ->
-          let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
-          log "WarningMsg" id;
-          add_flag sentence (`WARNING (loc, msg));
-          self#attach_tooltip sentence loc msg;
-          self#position_warning_tag_at_sentence sentence loc
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
@@ -520,18 +511,6 @@ object(self)
     let start, _, phrase = self#get_sentence sentence in
     self#position_error_tag_at_iter start phrase loc
 
-  method private position_warning_tag_at_iter iter_start iter_stop phrase loc =
-    if Loc.is_ghost loc then
-        buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop
-    else
-      buffer#apply_tag Tags.Script.warning
-	  ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp))
-          ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep))
-
-  method private position_warning_tag_at_sentence sentence loc =
-    let start, stop, phrase = self#get_sentence sentence in
-    self#position_warning_tag_at_iter start stop phrase loc
-
   method private process_interp_error queue sentence loc msg tip id =
     Coq.bind (Coq.return ()) (function () ->
     let start, stop, phrase = self#get_sentence sentence in
diff --git a/ide/sentence.ml b/ide/sentence.ml
index e332682dd0..6897779e80 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -16,7 +16,6 @@
 let split_slice_lax (buffer:GText.buffer) start stop =
   buffer#remove_tag ~start ~stop Tags.Script.sentence;
   buffer#remove_tag ~start ~stop Tags.Script.error;
-  buffer#remove_tag ~start ~stop Tags.Script.warning;
   buffer#remove_tag ~start ~stop Tags.Script.error_bg;
   let slice = buffer#get_text ~start ~stop () in
   let apply_tag off tag =
diff --git a/ide/session.ml b/ide/session.ml
index e998337604..cdec392ecc 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -195,8 +195,12 @@ let set_buffer_handlers
          to a point indicated by coq. *)
       if !no_coq_action_required then begin
         let start, stop = get_start (), get_stop () in
-	List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
-		  Tags.Script.ephemere;
+        buffer#remove_tag Tags.Script.error ~start ~stop;
+        buffer#remove_tag Tags.Script.error_bg ~start ~stop;
+        buffer#remove_tag Tags.Script.tooltip ~start ~stop;
+        buffer#remove_tag Tags.Script.processed ~start ~stop;
+        buffer#remove_tag Tags.Script.to_process ~start ~stop;
+        buffer#remove_tag Tags.Script.incomplete ~start ~stop;
         Sentence.tag_on_insert buffer
       end;
     end in
diff --git a/ide/tags.ml b/ide/tags.ml
index e4510e7af4..9ccff9fb51 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -18,7 +18,6 @@ struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
   let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
-  let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"]
   let error_bg = make_tag table ~name:"error_bg" []
   let to_process = make_tag table ~name:"to_process" []
   let processed = make_tag table ~name:"processed" []
@@ -30,11 +29,9 @@ struct
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
 
-  let ephemere =
-    [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified]
-
   let all =
-    comment :: found :: sentence :: ephemere
+    [comment; error; error_bg; to_process; processed; incomplete; unjustified;
+     found; sentence; tooltip]
 
   let edit_zone =
     let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
diff --git a/ide/tags.mli b/ide/tags.mli
index 02e15a5ae4..5a932f3300 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -11,7 +11,6 @@ sig
   val table : GText.tag_table
   val comment : GText.tag
   val error : GText.tag
-  val warning : GText.tag
   val error_bg : GText.tag
   val to_process : GText.tag
   val processed : GText.tag
@@ -21,7 +20,6 @@ sig
   val sentence : GText.tag
   val tooltip : GText.tag
   val edit_zone : GText.tag (* for debugging *)
-  val ephemere : GText.tag list
   val all : GText.tag list
 end
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74de6f67ff..5c5a900fba 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1166,6 +1166,10 @@ let alias_of als = match als.alias_ids with
 | [] -> Anonymous
 | id :: _ -> Name id
 
+let message_redundant_alias id1 id2 =
+  Feedback.msg_warning
+    (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
+
 (** {6 Expanding notations }
 
     @returns a raw_case_pattern_expr :
@@ -1738,6 +1742,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
+      Id.Map.iter message_redundant_alias asubst;
       let rhs' = intern {env with ids = env_ids} rhs in
       (loc,eqn_ids,pl,rhs')) pll
 
diff --git a/interp/notation.ml b/interp/notation.ml
index b0a2192004..e777e5c24e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -190,8 +190,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 ->
-        (** FIXME: implement multikey scopes? *)
-	Flags.if_verbose Feedback.msg_info
+	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;
@@ -199,7 +198,7 @@ let declare_delimiters scope key =
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      Flags.if_verbose Feedback.msg_info (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
@@ -208,7 +207,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> Errors.errorlabstrm "" (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
@@ -387,12 +386,6 @@ let level_of_notation ntn =
 
 (* The mapping between notations and their interpretation *)
 
-let warn_notation_overridden =
-  CWarnings.create ~name:"notation-overridden" ~category:"parsing"
-                   (fun (ntn,which_scope) ->
-                    str "Notation" ++ spc () ++ str ntn ++ spc ()
-                    ++ strbrk "was already used" ++ which_scope)
-
 let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
@@ -400,8 +393,8 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
     if String.Map.mem ntn sc.notations then
     let which_scope = match scopt with
     | None -> mt ()
-    | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
-    warn_notation_overridden (ntn,which_scope)
+    | Some _ -> str " in scope " ++ str scope in
+    Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
   let notdata = {
     not_interp = pat;
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7170fd14a5..9a1483b105 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -84,26 +84,23 @@ let declare_syntactic_definition local id onlyparse pat =
 
 let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
 
-let verbose_compat_notations = ref true
+let allow_compat_notations = ref true
+let verbose_compat_notations = ref false
 
 let is_verbose_compat () =
-  !verbose_compat_notations
-
-let pr_compat_warning (kn, def, v) =
-  let pp_def = match def with
-    | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
-    | _ -> strbrk " is a compatibility notation"
-  in
-  let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
-  pr_syndef kn ++ pp_def ++ since
-
-let warn_compatibility_notation =
-  CWarnings.create ~name:"compatibility-notation"
-                   ~category:"deprecated" pr_compat_warning
+  !verbose_compat_notations || not !allow_compat_notations
 
 let verbose_compat kn def = function
   | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
-     warn_compatibility_notation (kn, def, v)
+    let act =
+      if !verbose_compat_notations then Feedback.msg_warning ?loc:None else errorlabstrm ""
+    in
+    let pp_def = match def with
+      | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
+      | _ -> str " is a compatibility notation"
+    in
+    let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
+    act (pr_syndef kn ++ pp_def ++ since)
   | _ -> ()
 
 let search_syntactic_definition kn =
@@ -122,3 +119,12 @@ let set_verbose_compat_notations =
       optkey   = ["Verbose";"Compat";"Notations"];
       optread  = (fun () -> !verbose_compat_notations);
       optwrite = ((:=) verbose_compat_notations) }
+
+let set_compat_notations =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "accept compatibility notations";
+      optkey   = ["Compat"; "Notations"];
+      optread  = (fun () -> !allow_compat_notations);
+      optwrite = ((:=) allow_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index aa2c9c3c1b..7a1c9c5cb4 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,5 +18,8 @@ val declare_syntactic_definition : bool -> Id.t ->
 
 val search_syntactic_definition : kernel_name -> syndef_interpretation
 
-(** Option concerning verbose display of compatibility notations  *)
+(** Options concerning verbose display of compatibility notations
+    or their deactivation *)
+
 val set_verbose_compat_notations : bool -> unit
+val set_compat_notations : bool -> unit
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8cbc3ab445..a0ef5e570e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,8 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
       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
-	       (fun x -> Feedback.msg_warning x) in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None 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/nativeconv.ml b/kernel/nativeconv.ml
index 2f985e15ac..a0ff9e123a 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -145,16 +145,11 @@ let native_conv_gen pb sigma env univs t1 t2 =
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
-let warn_no_native_compiler =
-  let open Pp in
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-         (fun () -> strbrk "Native compiler is disabled," ++
-                      strbrk " falling back to VM conversion test.")
-
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
-    warn_no_native_compiler ();
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
+    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 d4a67b3999..5b92e9554f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -55,15 +55,6 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
-let warn_native_compiler_failed =
-  let print = function
-  | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
-  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
-  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
-  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
-  in
-  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
-
 let call_compiler ml_filename =
   let load_path = !get_load_paths () in
   let load_path = List.map (fun dn -> dn / output_dir) load_path in
@@ -87,12 +78,15 @@ let call_compiler ml_filename =
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        warn_native_compiler_failed (Inl res); false
-    in
+      | Unix.WEXITED n ->
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
+      | Unix.WSIGNALED n ->
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
+      | Unix.WSTOPPED n ->
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    warn_native_compiler_failed (Inr e);
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 710bfa19b8..30a346c910 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -676,18 +676,12 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
 let vm_conv = ref (fun cv_pb env ->
 		   gen_conv cv_pb env ~evars:((fun _->None), universes env))
 
-let warn_bytecode_compiler_failed =
-  let open Pp in
-  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
-         (fun () -> strbrk "Bytecode compiler failed, " ++
-                      strbrk "falling back to standard conversion")
-
 let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    warn_bytecode_compiler_failed ();
+    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/reduction.mli b/kernel/reduction.mli
index 3896446925..1b5e5e32a3 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -106,5 +106,3 @@ exception NotArity
 
 val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
-
-val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c729a6ce29..53db6f5bee 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,9 +185,10 @@ 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 _ ->
-    warn_bytecode_compiler_failed ();
-    Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      full_transparent_state env univs t1 t2
+    (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)
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b42429..096305b987 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -87,7 +87,8 @@ let load_aux_file_for vfile =
   | End_of_file -> !h
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
-    Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
+     Flags.if_verbose
+       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/cWarnings.ml b/lib/cWarnings.ml
deleted file mode 100644
index 7436dfd147..0000000000
--- a/lib/cWarnings.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-
-type status =
-  Disabled | Enabled | AsError
-
-type t = {
-  default : status;
-  category : string;
-  status : status;
-}
-
-let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
-let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
-
-let current_loc = ref Loc.ghost
-let flags = ref ""
-
-let set_current_loc = (:=) current_loc
-
-let get_flags () = !flags
-
-let add_warning_in_category ~name ~category =
-  let ws =
-    try
-      Hashtbl.find categories category
-    with Not_found -> []
-  in
-  Hashtbl.replace categories category (name::ws)
-
-let create ~name ~category ?(default=Enabled) pp =
-  Hashtbl.add warnings name { default; category; status = default };
-  add_warning_in_category ~name ~category;
-  if default <> Disabled then
-    add_warning_in_category ~name ~category:"default";
-  fun ?loc x -> let w = Hashtbl.find warnings name in
-           match w.status with
-           | Disabled -> ()
-           | AsError ->
-              let loc = Option.default !current_loc loc in
-              Errors.user_err_loc (loc,"_",pp x)
-           | Enabled ->
-              let msg =
-                pp x ++ str " [" ++ str name ++ str "," ++
-                  str category ++ str "]"
-              in
-              let loc = Option.default !current_loc loc in
-              Feedback.msg_warning ~loc msg
-
-let warn_unknown_warning =
-  create ~name:"unknown-warning" ~category:"toplevel"
-         (fun name -> strbrk "Unknown warning name: " ++ str name)
-
-let set_warning_status ~name status =
-  try
-    let w = Hashtbl.find warnings name in 
-    Hashtbl.replace warnings name { w with status = status }
-  with Not_found -> warn_unknown_warning name
-
-let reset_default_warnings () =
-  Hashtbl.filter_map_inplace (fun name w -> Some { w with status = w.default }) warnings
-
-let set_all_warnings_status status =
-  Hashtbl.filter_map_inplace (fun name w -> Some { w with status }) warnings
-
-let parse_flag s =
-  if String.length s > 1 then
-    match String.get s 0 with
-    | '+' -> (AsError, String.sub s 1 (String.length s - 1))
-    | '-' -> (Disabled, String.sub s 1 (String.length s - 1))
-    | _ -> (Enabled, s)
-  else Errors.error "Invalid warnings flag"
-
-let rec do_all_keyword = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     if String.equal name "all" then
-       (set_all_warnings_status status; do_all_keyword items)
-     else item :: do_all_keyword items
-
-let rec do_categories = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     try
-       let names = Hashtbl.find categories name in
-       List.iter (fun name -> set_warning_status name status) names;
-       do_categories items
-     with Not_found -> item :: do_categories items
-
-let rec parse_warnings items =
-  List.iter (fun (status, name) -> set_warning_status ~name status) items
-
-(* For compatibility, we accept "none" *)
-let parse_flags s = 
-  if String.equal s "none" then begin
-      Flags.make_warn false;
-      set_all_warnings_status Disabled
-    end
-  else begin
-      Flags.make_warn true;
-      let reg = Str.regexp "[ ,]+" in
-      let items = List.map parse_flag (Str.split reg s) in
-      let items = do_all_keyword items in
-      let items = do_categories items in
-      parse_warnings items
-    end
-
-let set_flags s =
-  flags := s; reset_default_warnings (); parse_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
deleted file mode 100644
index 3515542840..0000000000
--- a/lib/cWarnings.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type status =
-  Disabled | Enabled | AsError
-
-(*
-type 'a repr = {
-  print : 'a -> Pp.std_ppcmds;
-  kind : string;
-  enabled : bool;
-}
- *)
-
-val set_current_loc : Loc.t -> unit
-
-val create : name:string -> category:string -> ?default:status ->
-             ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
-
-(*
-val emit : 'a t -> 'a -> unit
-
-type any = Any : string * string * 'a repr -> any
-
-val dump : unit -> any list
- *)
-
-val get_flags : unit -> string
-val set_flags : string -> unit
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 0ec3b2ebe4..bedbe226c2 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -80,33 +80,31 @@ let info_str = mt ()
 let warn_str = str "Warning:" ++ spc ()
 let  err_str = str "Error:"   ++ spc ()
 
-let make_body quoter info ?loc s =
-  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  quoter (hov 0 (loc ++ info ++ s))
+let make_body quoter info s = quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
 let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl (make_body dbg  dbg_str ?loc msg)
-  | Info    -> msgnl (make_body dbg info_str ?loc msg)
-  (* XXX: What to do with loc here? *)
+  | 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 ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
+               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 ?loc level strm =
-  let msg  = Ppstyle.color_msg in
+  let msg = Ppstyle.color_msg in
   match level with
-  | Debug   -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
-  | Info    -> msg ?loc !std_ft strm
-  | Notice  -> msg ?loc !std_ft strm
-  | Warning -> Flags.if_warn (fun () ->
-               msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
-  | Error   -> msg ?loc ~header:("Error",   Ppstyle.error_tag)   !err_ft strm
+  | 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
@@ -118,11 +116,11 @@ 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    ?loc x = !logger ?loc Info x
-let msg_notice  ?loc x = !logger ?loc Notice x
-let msg_warning ?loc x = !logger ?loc Warning x
-let msg_error   ?loc x = !logger ?loc Error x
-let msg_debug   ?loc x = !logger ?loc Debug x
+let msg_info    ?loc x = !logger Info x
+let msg_notice  ?loc x = !logger Notice x
+let msg_warning ?loc x = !logger Warning x
+let msg_error   ?loc x = !logger Error x
+let msg_debug   ?loc x = !logger Debug x
 
 (** Feeders *)
 let feeder = ref ignore
diff --git a/lib/flags.ml b/lib/flags.ml
index 13525165ab..ba19c7a63b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -172,7 +172,7 @@ let make_polymorphic_flag b =
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
-let warn = ref true
+let warn = ref false
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 4b13156d60..a6c09058dd 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,5 +1,4 @@
 Errors
-CWarnings
 Bigint
 Segmenttree
 Unicodetable
diff --git a/lib/pp.ml b/lib/pp.ml
index 1cef69fcc3..d07f01b906 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -197,25 +197,6 @@ let strbrk s =
     else if p = n then [] else [str (String.sub s p (n-p))]
   in List.fold_left (++) Glue.empty (aux 0 0)
 
-let pr_loc_pos loc =
-  if Loc.is_ghost loc then (str"<unknown>")
-  else
-    let loc = Loc.unloc loc in
-    int (fst loc) ++ str"-" ++ int (snd loc)
-
-let pr_loc loc =
-  if Loc.is_ghost loc then str"<unknown>"
-  else
-    let fname = loc.Loc.fname in
-    if String.equal fname "" then
-      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
-	   str"-" ++ int loc.ep ++ str":" ++ fnl ())
-    else
-      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-	   str", line " ++ int loc.line_nb ++ str", characters " ++
-	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
-	   str":" ++ fnl())
-
 let ismt = is_empty
 
 (* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 3bd560812e..a18744c376 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -166,8 +166,6 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
-val pr_loc : Loc.t -> std_ppcmds
-
 (** {6 Low-level pretty-printing functions with and without flush} *)
 
 (** FIXME: These ignore the logging settings and call [Format] directly *)
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index ecfaa822c7..b068788c92 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -124,16 +124,15 @@ let init_color_output () =
   Format.pp_set_formatter_tag_functions !std_ft tag_handler;
   Format.pp_set_formatter_tag_functions !err_ft tag_handler
 
-let color_msg ?loc ?header ft strm =
+let color_msg ?header ft strm =
   let pptag = tag in
   let open Pp in
-  let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
   let strm = match header with
-    | None -> hov 0 (ploc ++ strm)
+    | 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 (ploc ++ h ++ spc () ++ strm)
+      hov 0 (h ++ spc () ++ strm)
   in
   pp_with ~pp_tag ft strm;
   Format.pp_print_newline ft ();
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index b07fcd5d4c..1cd701ed4e 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -48,7 +48,7 @@ val dump : unit -> (t * Terminal.style option) list
 
 val init_color_output : unit -> unit
 
-val color_msg : ?loc:Loc.t -> ?header:string * Format.tag ->
+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 *)
diff --git a/lib/system.ml b/lib/system.ml
index b27918522c..8b53a11d67 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -18,10 +18,6 @@ include Minisys
     depth-first search, with sons ordered as on the file system;
     warns if [root] does not exist *)
 
-let warn_cannot_open_dir =
-  CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
-  (fun dir -> str ("Cannot open directory " ^ dir))
-
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
@@ -36,7 +32,7 @@ let all_subdirs ~unix_path:root =
   in
   check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
-  else warn_cannot_open_dir root;
+  else Feedback.msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -89,22 +85,19 @@ let rec search paths test =
   | [] -> []
   | lpe :: rem -> test lpe @ search rem test
 
-let warn_ambiguous_file_name =
-  CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
-    (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
-                hov 0 (str "[ " ++
-                         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
-                                               (fun (lpe,_) -> str lpe) l)
-                       ++ str " ];") ++ fnl () ++
-                str "loading " ++ str f)
-
-
 let where_in_path ?(warn=true) path filename =
   let check_and_warn l = match l with
   | [] -> raise Not_found
   | (lpe, f) :: l' ->
     let () = match l' with
-    | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
+    | _ :: _ when warn ->
+      Feedback.msg_warning
+        (str filename ++ str " has been found in" ++ spc () ++
+          hov 0 (str "[ " ++
+            hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+              (fun (lpe,_) -> str lpe) l)
+            ++ str " ];") ++ fnl () ++
+          str "loading " ++ str f)
     | _ -> ()
     in
     (lpe, f)
@@ -149,16 +142,12 @@ let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
-let warn_path_not_found =
-  CWarnings.create ~name:"path-not-found" ~category:"filesystem"
-  (fun () -> str "system variable PATH not found")
-
 let is_in_system_path filename =
   try
     let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
     is_in_path lpath filename
   with Not_found ->
-    warn_path_not_found ();
+    Feedback.msg_warning (str "system variable PATH not found");
     false
 
 let open_trapping_failure name =
@@ -166,14 +155,11 @@ let open_trapping_failure name =
   with e when Errors.noncritical e ->
     errorlabstrm "System.open" (str "Can't open " ++ str name)
 
-let warn_cannot_remove_file =
-  CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
-  (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
-
 let try_remove filename =
   try Sys.remove filename
   with e when Errors.noncritical e ->
-    warn_cannot_remove_file filename
+    Feedback.msg_warning
+      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let error_corrupted file s =
   errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
diff --git a/library/goptions.ml b/library/goptions.ml
index 7bead0b63d..4aa3a2a21d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -233,11 +233,6 @@ with Not_found ->
 open Libobject
 open Lib
 
-let warn_deprecated_option =
-  CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
-         (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
-                       strbrk " is deprecated")
-
 let declare_option cast uncast
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
@@ -275,7 +270,10 @@ let declare_option cast uncast
     begin fun v -> add_anonymous_leaf (gdecl_obj v) end
   else write,write,write
   in
-  let warn () = if depr then warn_deprecated_option key in
+  let warn () =
+    if depr then
+      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
   let clwrite v = warn (); lwrite (uncast v) in
@@ -306,22 +304,19 @@ let declare_stringopt_option =
 
 (* Setting values of options *)
 
-let warn_unknown_option =
-  CWarnings.create ~name:"unknown-option" ~category:"option"
-                   (fun key -> strbrk "There is no option " ++
-                                 str (nickname key) ++ str ".")
-
 let set_option_value locality check_and_cast key v =
-  let opt = try Some (get_option key) with Not_found -> None in
-  match opt with
-  | None -> warn_unknown_option key
-  | Some (name, depr, (_,read,write,lwrite,gwrite)) ->
-    let write = match locality with
-      | None -> write
-      | Some true -> lwrite
-      | Some false -> gwrite
-    in
-    write (check_and_cast v (read ()))
+  let (name, depr, (_,read,write,lwrite,gwrite)) =
+    try get_option key
+    with Not_found ->
+      errorlabstrm "Goptions.set_option_value"
+        (str "There is no option " ++ str (nickname key) ++ str ".")
+  in
+  let write = match locality with
+    | None -> write
+    | Some true -> lwrite
+    | Some false -> gwrite
+  in
+  write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option."
 
@@ -351,11 +346,13 @@ let check_unset_value v = function
 let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
-  set_option_value locality check_bool_value key v
+  try set_option_value locality check_bool_value key v
+  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 =
-  set_option_value locality check_unset_value key ()
+  try set_option_value locality check_unset_value key ()
+  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
diff --git a/library/libobject.ml b/library/libobject.ml
index 3e08b38b12..b12d2038ae 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -12,6 +12,18 @@ open Util
 
 module Dyn = Dyn.Make(struct end)
 
+(* The relax flag is used to make it possible to load files while ignoring
+   failures to incorporate some objects.  This can be useful when one
+   wants to work with restricted Coq programs that have only parts of
+   the full capabilities, but may still be able to work correctly for
+   limited purposes.  One example is for the graphical interface, that uses
+   such a limited Coq process to do only parsing.  It loads .vo files, but
+   is only interested in loading the grammar rule definitions. *)
+
+let relax_flag = ref false;;
+
+let relax b = relax_flag := b;;
+
 type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
@@ -102,16 +114,31 @@ let declare_object_full odecl =
   try declare_object_full odecl
   with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
 
+let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
+
 (* this function describes how the cache, load, open, and export functions
-   are triggered. *)
+   are triggered.  In relaxed mode, this function just return a meaningless
+   value instead of raising an exception when they fail. *)
 
 let apply_dyn_fun deflt f lobj =
   let tag = object_tag lobj in
-  let dodecl =
-    try Hashtbl.find cache_tab tag
-    with Not_found -> assert false
-  in
-  f dodecl
+  try
+    let dodecl =
+      try
+        Hashtbl.find cache_tab tag
+      with Not_found ->
+        failwith "local to_apply_dyn_fun" in
+    f dodecl
+  with
+    Failure "local to_apply_dyn_fun" ->
+      if not (!relax_flag || Hashtbl.mem missing_tab tag) then
+        begin
+          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 ()
+        end;
+      deflt
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 51b9af059f..dbe0de8f8a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -107,6 +107,7 @@ val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
+val relax : bool -> unit
 
 (** {6 Debug} *)
 
diff --git a/library/library.ml b/library/library.ml
index cead907009..bc7723f481 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -271,12 +271,6 @@ exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
-let warn_several_object_files =
-  CWarnings.create ~name:"several-object-files" ~category:"require"
-         (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
-                            strbrk " instead of " ++ str vo ++
-                            strbrk " because it is more recent")
-
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
@@ -293,8 +287,9 @@ let locate_absolute_library dir =
   | [] -> raise LibNotFound
   | [file] -> file
   | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-    warn_several_object_files (vi, vo);
-    vi
+       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+         str vo ++ str " because it is more recent");
+       vi
   | [vo;vi] -> vo
   | _ -> assert false
 
@@ -316,7 +311,8 @@ 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) ->
-      warn_several_object_files (vi, vo);
+       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
     | _ -> assert false
@@ -757,7 +753,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 () = Feedback.msg_notice (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 6f4d79430d..33c0f41e17 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -50,13 +50,6 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
-let warn_overriding_logical_loadpath =
-  CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
-         (fun (phys_path, old_path, coq_path) ->
-          str phys_path ++ strbrk " was previously bound to " ++
-            pr_dirpath old_path ++ strbrk "; it is remapped to " ++
-            pr_dirpath coq_path)
-
 let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
@@ -79,8 +72,10 @@ 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
-          warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
-        in
+            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
         true in
     if replace then
       begin
diff --git a/library/nametab.ml b/library/nametab.ml
index f533bc7914..db902d625b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -82,14 +82,6 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE
 struct
   type elt = E.t
 
-  (* A name became inaccessible, even with absolute qualification.
-     Example:
-     Module F (X : S). Module X.
-     The argument X of the functor F is masked by the inner module X.
-   *)
-  let masking_absolute n =
-    Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"))
-
   type user_name = U.t
 
   type path_status =
@@ -127,7 +119,9 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-                masking_absolute n; tree.path
+		    Feedback.msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
+		  tree.path
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
           else tree.path
@@ -150,6 +144,7 @@ struct
 	  | Nothing
 	  | Relative _ -> mktree (Absolute (uname,o)) tree.map
 
+
 let rec push_exactly uname o level tree = function
 | [] ->
   anomaly (Pp.str "Prefix longer than path! Impossible!")
@@ -160,7 +155,9 @@ 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 *)
-            masking_absolute n; tree.path
+              Feedback.msg_warning (str ("Trying to mask the absolute name \""
+                        ^ U.to_string n ^ "\"!"));
+            tree.path
         | Nothing
         | Relative _ -> Relative (uname,o)
     in
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index b5494a7cbb..517f9e3afd 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -72,11 +72,6 @@ let test_bracket_ident =
 
 (* Tactics grammar rules *)
 
-let warn_deprecated_appcontext =
-  CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated"
-         (fun () -> strbrk "appcontext is deprecated and will be removed " ++
-                      strbrk "in a future version")
-
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
           tactic_mode constr_may_eval constr_eval selector toplevel_selector;
@@ -237,7 +232,7 @@ GEXTEND Gram
         Subterm (mode, oid, pc)
       | IDENT "appcontext";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        warn_deprecated_appcontext ~loc:!@loc ();
+        Feedback.msg_warning (strbrk "appcontext is deprecated");
         Subterm (true,oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index f332e1a0d5..9081fd3e92 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -32,14 +32,10 @@ let is_new_call () = let b = !new_call in new_call := false; b
     profiling results will be off. *)
 let encountered_multi_success_backtracking = ref false
 
-let warn_profile_backtracking =
-  CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
-    (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
-            into multi-success tactics; profiling results may be wildly inaccurate.")
-
 let warn_encountered_multi_success_backtracking () =
   if !encountered_multi_success_backtracking then
-    warn_profile_backtracking ()
+    Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \
+    into multi-success tactics; profiling results may be wildly inaccurate.")
 
 let encounter_multi_success_backtracking () =
   if not !encountered_multi_success_backtracking
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 6b7ae21f3c..f00adecf2a 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -417,11 +417,6 @@ type tacdef_kind =
 let is_defined_tac kn =
   try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
 
-let warn_unusable_identifier =
-  CWarnings.create ~name:"unusable-identifier" ~category:"parsing"
-      (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++
-        strbrk "may be unusable because of a conflict with a notation.")
-
 let register_ltac local tacl =
   let map tactic_body =
     match tactic_body with
@@ -432,14 +427,17 @@ let register_ltac local tacl =
           Errors.user_err_loc (loc, "",
             str "There is already an Ltac named " ++ id_pp ++ str".")
         in
-        let is_shadowed =
+        let is_primitive =
           try
             match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with
             | Tacexpr.TacArg _ -> false
             | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
           with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
         in
-        let () = if is_shadowed then warn_unusable_identifier id in
+        let () = if is_primitive then
+          Feedback.msg_warning (str "The Ltac name " ++ id_pp ++
+            str " may be unusable because of a conflict with a notation.")
+        in
         NewTac id, body
     | TacticRedefinition (ident, body) ->
         let loc = loc_of_reference ident in
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index e3d5e18c9d..005d1f5f48 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -53,7 +53,8 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
   let () =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
-        tac_tab := MLTacMap.remove s !tac_tab
+        let () = tac_tab := MLTacMap.remove s !tac_tab in
+        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 9a4beed871..e814cc7e67 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1144,12 +1144,6 @@ let rec read_match_rule lfun ist env sigma = function
       :: read_match_rule lfun ist env sigma tl
   | [] -> []
 
-let warn_deprecated_info =
-  CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated"
-         (fun () ->
-          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.")
 
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
@@ -1257,7 +1251,10 @@ 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 ->
-      warn_deprecated_info ();
+      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.");
       eval_tactic ist tac
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 711d2240ba..b04c7633a9 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -206,16 +206,12 @@ let check_keyword str =
   in
   loop_symb (Stream.of_string str)
 
-let warn_unparsable_keyword =
-  CWarnings.create ~name:"unparsable-keyword" ~category:"parsing"
-         (fun (s,unicode) ->
-          strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
-                                  which will not be parsable." s unicode))
-            
 let check_keyword_to_add s =
   try check_keyword s
   with Error.E (UnsupportedUnicode unicode) ->
-    warn_unparsable_keyword (s,unicode)
+    Flags.if_verbose Feedback.msg_warning
+      (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
+                               which will not be parsable." s unicode))
 
 let check_ident str =
   let rec loop_id intail = parser
@@ -320,14 +316,6 @@ let rec number_or_index loc bp l len = parser
       | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len
       | _ -> true, len
 
-let warn_comment_terminator_in_string =
-  CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
-         (fun () ->
-          (strbrk
-             "Not interpreting \"*)\" as the end of current \
-              non-terminated comment because it occurs in a \
-              non-terminated string of the comment."))
-
 (* If the string being lexed is in a comment, [comm_level] is Some i with i the
    current level of comments nesting. Otherwise, [comm_level] is None. *)
 let rec string loc ~comm_level bp len = parser
@@ -347,7 +335,11 @@ let rec string loc ~comm_level bp len = parser
         | [< '')'; s >] ->
             let () = match comm_level with
             | Some 0 ->
-	       warn_comment_terminator_in_string ~loc:!@loc ()
+                Feedback.msg_warning
+                  (strbrk
+                     "Not interpreting \"*)\" as the end of current \
+                      non-terminated comment because it occurs in a \
+                      non-terminated string of the comment.")
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8a83bc2d1d..d0bca9ee3f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -211,10 +211,6 @@ let merge_occurrences loc cl = function
     in
     (Some p, ans)
 
-let warn_deprecated_eqn_syntax =
-  CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
-         (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
-
 (* Auxiliary grammar rules *)
 
 GEXTEND Gram
@@ -473,11 +469,11 @@ GEXTEND Gram
   eqn_ipat:
     [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
-         let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
+        let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in
+        Feedback.msg_warning (strbrk msg); Some (!@loc, pat)
       | IDENT "_eqn" ->
-         let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
+        let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
+        Feedback.msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ecbe3ac969..f0475ee25b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -123,18 +123,16 @@ GEXTEND Gram
   ;
 END
 
-let warn_plural_command =
-  CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:Disabled
-         (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd))
-
-let test_plural_form loc kwd = function
+let test_plural_form = function
   | [(_,([_],_))] ->
-     warn_plural_command ~loc:!@loc kwd
+      Flags.if_verbose Feedback.msg_warning
+   (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption")
   | _ -> ()
 
-let test_plural_form_types loc kwd = function
+let test_plural_form_types = function
   | [([_],_)] ->
-     warn_plural_command ~loc:!@loc kwd
+      Flags.if_verbose Feedback.msg_warning
+   (strbrk "Keywords Implicit Types expect more than one type")
   | _ -> ()
 
 let fresh_var env c =
@@ -157,8 +155,8 @@ GEXTEND Gram
           VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
-      | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
-	  test_plural_form loc kwd bl;
+      | stre = assumptions_token; nl = inline; bl = assum_list ->
+	  test_plural_form bl;
 	  VernacAssumption (stre, nl, bl)
       | d = def_token; id = pidentref; b = def_body ->
           VernacDefinition (d, id, b)
@@ -211,11 +209,11 @@ GEXTEND Gram
       | IDENT "Conjecture" -> (None, Conjectural) ] ]
   ;
   assumptions_token:
-    [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical))
-      | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional))
-      | kwd = IDENT "Axioms" -> (kwd, (None, Logical))
-      | kwd = IDENT "Parameters" -> (kwd, (None, Definitional))
-      | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ]
+    [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
+      | IDENT "Variables" -> (Some Discharge, Definitional)
+      | IDENT "Axioms" -> (None, Logical)
+      | IDENT "Parameters" -> (None, Definitional)
+      | IDENT "Conjectures" -> (None, Conjectural) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
@@ -424,10 +422,6 @@ let starredidentreflist_to_expr l =
   | [] -> SsEmpty
   | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x
 
-let warn_deprecated_include_type =
-  CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated"
-         (fun () -> strbrk "Include Type is deprecated; use Include instead")
-
 (* Modules and Sections *)
 GEXTEND Gram
   GLOBAL: gallina_ext module_expr module_type section_subset_expr;
@@ -467,8 +461,9 @@ GEXTEND Gram
       | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
-	 warn_deprecated_include_type ~loc:!@loc ();
-	 VernacInclude(e::l) ] ]
+	  Flags.if_verbose
+            Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead");
+          VernacInclude(e::l) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
@@ -572,14 +567,6 @@ GEXTEND Gram
   ;
 END
 
-let warn_deprecated_arguments_scope =
-  CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated"
-         (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead")
-
-let warn_deprecated_implicit_arguments =
-  CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated"
-         (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead")
-
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
   GLOBAL: gallina_ext instance_name;
@@ -694,21 +681,22 @@ 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 ]; "]" ->
-	warn_deprecated_arguments_scope ~loc:!@loc ();
+       Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
         VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	 warn_deprecated_implicit_arguments ~loc:!@loc ();
-	 VernacDeclareImplicits (qid,pos)
+	   Flags.if_verbose
+            Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
+	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
 	   VernacReserve bl
 
       | IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
-          test_plural_form_types loc "Implicit Types" bl;
+          test_plural_form_types bl;
            VernacReserve bl
 
       | IDENT "Generalizable"; 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 836f1982db..3fa600ac29 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -283,10 +283,6 @@ let register_automation_tac tac = my_automation_tac:= tac
 
 let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
 
-let warn_insufficient_justification =
-  CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
-    (fun () -> strbrk "Insufficient justification.")
-
 let justification tac gls=
     tclORELSE
       (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
@@ -295,7 +291,7 @@ let justification tac gls=
 	   error "Insufficient justification."
 	 else
 	   begin
-             warn_insufficient_justification ();
+	     Feedback.msg_warning (str "Insufficient justification.");
 	     daimon_tac gls
 	   end) gls
 
@@ -1223,9 +1219,6 @@ let hrec_for fix_id per_info gls obj_id =
   let hd2 = applist (mkVar fix_id,args@[obj]) in
     compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
 
-let warn_missing_case =
-  CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
-    (fun () -> strbrk "missing case")
 
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
@@ -1300,8 +1293,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	       end;
 	       match bro with
 		   None ->
-                     warn_missing_case ();
-                     tacnext (mkMeta 1)
+		     Feedback.msg_warning (str "missing case");
+		     tacnext (mkMeta 1)
 		 | Some (sub_ids,tree) ->
 		     let br_args =
 		       List.filter
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 94981d0e1f..a03be5743f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -583,8 +583,8 @@ let rec locate_ref = function
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-           warning_ambiguous_name (q,mp,r);
-           let refs,mps = locate_ref l in refs,mp::mps
+	    warning_both_mod_and_cst q mp r;
+	    let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 81dfa603dd..560fe5aea8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -295,94 +295,81 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 let err s = errorlabstrm "Extraction" s
 
-let warn_extraction_axiom_to_realize =
-  CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
-         (fun axioms ->
-          let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in
-          strbrk ("The following "^s^" must be realized in the extracted code:")
-                   ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms)
-                   ++ str "." ++ fnl ())
-
-let warn_extraction_logical_axiom =
-  CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction"
-         (fun axioms ->
-          let s =
-            if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were"
-          in
-          (strbrk ("The following logical "^s^" encountered:") ++
-             hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n")
-           ++ strbrk "Having invalid logical axiom in the environment when extracting"
-           ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++
-             fnl ()))
-
 let warning_axioms () =
   let info_axioms = Refset'.elements !info_axioms in
-  if not (List.is_empty info_axioms) then
-    warn_extraction_axiom_to_realize info_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
+    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 ())
+  end;
   let log_axioms = Refset'.elements !log_axioms in
-  if not (List.is_empty log_axioms) then
-    warn_extraction_logical_axiom log_axioms
-
-let warn_extraction_opaque_accessed =
-  CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction"
-    (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++
-                  strbrk "the following opaque constant bodies have been accessed :" ++
-                  lst ++ str "." ++ fnl ())
-
-let warn_extraction_opaque_as_axiom =
-  CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction"
-    (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++
-	 strbrk "the following opaque constants have been extracted as axioms :" ++
-	 lst ++ str "." ++ fnl () ++
-	 strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
-	 ++ fnl ())
+  if List.is_empty log_axioms then ()
+  else begin
+    let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
+    in
+    Feedback.msg_warning
+      (str ("The following logical "^s^" encountered:") ++
+       hov 1
+         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
+       ++
+       str "Having invalid logical axiom in the environment when extracting" ++
+       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
+       fnl ())
+  end
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if not (List.is_empty opaques) then
+  if List.is_empty opaques then ()
+  else
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
-    if accessed then warn_extraction_opaque_accessed lst
-    else warn_extraction_opaque_as_axiom lst
-
-let warning_ambiguous_name =
-  CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction"
-    (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++
-                       strbrk "do you mean module " ++
-                       pr_long_mp mp ++
-                       strbrk " or object " ++
-                       pr_long_global r ++ str " ?" ++ fnl () ++
-                       strbrk "First choice is assumed, for the second one please use " ++
-                       strbrk "fully qualified name." ++ fnl ())
+    if accessed then
+      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
+      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 () ++
+	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+	 ++ fnl ())
+
+let warning_both_mod_and_cst q mp r =
+ Feedback.msg_warning
+   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
+    str "do you mean module " ++
+    pr_long_mp mp ++
+    str " or object " ++
+    pr_long_global r ++ str " ?" ++ fnl () ++
+    str "First choice is assumed, for the second one please use " ++
+    str "fully qualified name." ++ fnl ())
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
        safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
-let warn_extraction_inside_module =
-  CWarnings.create ~name:"extraction-inside-module" ~category:"extraction"
-      (fun () -> strbrk "Extraction inside an opened module is experimental." ++
-       strbrk "In case of problem, close it first.")
-
-
 let check_inside_module () =
   if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
 	 str "Close it and try again.")
   else if Lib.is_module () then
-    warn_extraction_inside_module ()
+    Feedback.msg_warning
+      (str "Extraction inside an opened module is experimental.\n" ++
+       str "In case of problem, close it first.\n")
 
 let check_inside_section () =
   if Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
-let warn_extraction_reserved_identifier =
-  CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction"
-    (fun s -> strbrk ("The identifier "^s^
-                " contains __ which is reserved for the extraction"))
-
-let warning_id s = warn_extraction_reserved_identifier s
+let warning_id s =
+  Feedback.msg_warning (str ("The identifier "^s^
+		    " contains __ which is reserved for the extraction"))
 
 let error_constant r =
   err (safe_pr_global r ++ str " is not a constant.")
@@ -460,15 +447,12 @@ let error_remaining_implicit k =
        str "You might also try Unset Extraction SafeImplicits to force" ++
        fnl() ++ str "the extraction of unsafe code and review it manually.")
 
-let warn_extraction_remaining_implicit =
-  CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction"
-    (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
-     strbrk "Extraction SafeImplicits is unset, extracting nonetheless,"
-     ++ strbrk "but this code is potentially unsafe, please review it manually.")
-
 let warning_remaining_implicit k =
   let s = msg_of_implicit k in
-  warn_extraction_remaining_implicit s
+  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.")
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 15a08756c0..62c20bd3a7 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -21,7 +21,8 @@ val safe_basename_of_global : global_reference -> Id.t
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit
+val warning_both_mod_and_cst :
+ qualid -> module_path -> global_reference -> unit
 val warning_id : string -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 95095b09cb..cec3505a97 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -120,11 +120,6 @@ let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma p
 let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
-let warn_deprecated_syntax =
-  CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
-    (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
-
-
 ARGUMENT EXTEND firstorder_using
   TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
@@ -135,7 +130,8 @@ ARGUMENT EXTEND firstorder_using
 | [ "using" reference(a) ] -> [ [a] ]
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
 | [ "using" reference(a) reference(b) reference_list(l) ] -> [
-    warn_deprecated_syntax ();
+    Flags.if_verbose
+      Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
     a::b::l
   ]
 | [ ] -> [ [] ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 93a89330e3..893baad8c9 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -198,13 +198,15 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-       let names = pr_enum Libnames.pr_reference names in
-       let error = if do_observe () then (spc () ++ Errors.print e) else mt () in
-       warn_cannot_define_graph (names,error)
+	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 ->
-       let names = pr_enum Libnames.pr_reference names in
-       let error = if do_observe () then Errors.print e else mt () in
-       warn_cannot_define_principle (names,error)
+	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 ())
     | _ -> raise e
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ebbb34e4c..1c5eb16218 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -227,11 +227,6 @@ let prepare_body ((name,_,args,types,_),_) rt =
 let process_vernac_interp_error e =
   fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
 
-let warn_funind_cannot_build_inversion =
-  CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
-    (fun e' -> strbrk "Cannot build inversion information" ++
-                 if do_observe () then (fnl() ++ Errors.print e') else mt ())
-
 let derive_inversion fix_names =
   try
     let evd' = Evd.from_env (Global.env ()) in 
@@ -274,20 +269,14 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      warn_funind_cannot_build_inversion e'
+      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
-    warn_funind_cannot_build_inversion e'
-
-let warn_cannot_define_graph =
-  CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
-    (fun (names,error) -> strbrk "Cannot define graph(s) for " ++
-      h 1 names ++ error)
-
-let warn_cannot_define_principle =
-  CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind"
-  (fun (names,error) -> strbrk "Cannot define induction principle(s) for "++
-      h 1 names ++ error)
+      let e' = process_vernac_interp_error e in
+      Feedback.msg_warning
+	(str "Cannot build inversion information (early)" ++
+	   if do_observe () then (fnl() ++ Errors.print e') else mt ())       
 
 let warning_error names e =
   let e = process_vernac_interp_error e in
@@ -305,11 +294,15 @@ let warning_error names e =
   in
   match e with
     | Building_graph e ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_graph (names,e_explain e)
+      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 ->
-       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
-       warn_cannot_define_principle (names,e_explain e)
+      Feedback.msg_warning
+	(str "Cannot define principle(s) for "++
+	   h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+	   e_explain e)
     | _ -> raise e
 
 let error_error names e =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 1c27bdface..e720691406 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,9 +1,5 @@
 open Misctypes
 
-val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
-
-val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
-
 val do_generate_principle :  
   bool -> 
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> 
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 89305838b1..3142c8cf00 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -26,16 +26,14 @@ open Errors
 
 let threshold = of_int 5000
 
-let warn_large_nat =
-  CWarnings.create ~name:"large-nat" ~category:"numbers"
-    (fun () -> 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 " ++
-                 strbrk "limits and on the command executed).")
-
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than threshold n then warn_large_nat ();
+      if less_than threshold n then
+	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 " ++
+	   strbrk "limits and on the command executed).");
       let ref_O = GRef (dloc, glob_O, None) in
       let ref_S = GRef (dloc, glob_S, None) in
       let rec mk_nat acc n =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d3d4201f57..55220f44c0 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
-    Feedback.msg_info (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 c566839e85..129725c6d2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t
 
 exception PatternMatchingFailure
 
-let warn_meta_collision =
-  CWarnings.create ~name:"meta-collision" ~category:"ltac"
-         (fun name ->
-          strbrk "Collision between bound variable " ++ pr_id name ++
-            strbrk " and a metavariable of same name.")
+let warn_bound_meta name =
+  Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++
+    str " and a metavariable of same name.")
 
+let warn_bound_bound 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
@@ -62,19 +62,18 @@ let constrain n (ids, m as x) (names, terms as subst) =
     if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
-    let () = if Id.Map.mem n names then warn_meta_collision n in
+    let () = if Id.Map.mem n names then warn_bound_meta n in
     (names, Id.Map.add n x terms)
 
 let add_binders na1 na2 binding_vars (names, terms as subst) =
   match na1, na2 with
   | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
     if Id.Map.mem id1 names then
-      let () = Glob_ops.warn_variable_collision id1 in
+      let () = warn_bound_bound id1 in
       (names, terms)
     else
       let names = Id.Map.add id1 id2 names in
-      let () = if Id.Map.mem id1 terms then
-        warn_meta_collision id1 in
+      let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
       (names, terms)
   | _ -> subst
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc178eb975..86921c49b0 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 Feedback.msg_debug (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/glob_ops.ml b/pretyping/glob_ops.ml
index 5c8060996a..04100c8a73 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -334,14 +334,10 @@ let glob_visible_short_qualid c =
         fold_glob_constr aux acc c
   in aux [] c
 
-let warn_variable_collision =
-  let open Pp in
-  CWarnings.create ~name:"variable-collision" ~category:"ltac"
-         (fun name ->
-          strbrk "Collision between bound variables of name " ++ pr_id name)
-
 let add_and_check_ident id set =
-  if Id.Set.mem id set then warn_variable_collision id;
+  if Id.Set.mem id set then
+    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/glob_ops.mli b/pretyping/glob_ops.mli
index c2b27ca6ab..e0a2de0326 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -34,8 +34,6 @@ val map_glob_constr :
 val map_glob_constr_left_to_right :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
-val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
-
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index fc38e98c63..5d36fc78ef 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -183,7 +183,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
               | ra::rest ->
                   (match dest_recarg ra with
 	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
-	            | Imbr _  -> (None,rest)
+	            | Imbr _  ->
+		        Feedback.msg_warning (strbrk "Ignoring recursive call");
+		        (None,rest)
                     | _ -> (None, rest))
 	  in
           (match optionpos with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3344faef8a..d6305d81a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -348,7 +348,8 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Errors.error ("Cast not supported 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,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2959bd7c84..bbb6a92663 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -187,13 +187,6 @@ let cs_pattern_of_constr t =
           with e when Errors.noncritical e -> raise Not_found
 	end
 
-let warn_projection_no_head_constant =
-  CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (t,con_pp,proji_sp_pp) ->
-          strbrk "Projection value has no head constant: "
-          ++ Termops.print_constr t ++ strbrk " in canonical instance "  
-          ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
-
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
@@ -220,10 +213,13 @@ let compute_canonical_projections (con,ind) =
 		   let patt, n , args = cs_pattern_of_constr t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
-                     let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
+                   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
-                     warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
-                   l
+		      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
 	       end
 	   | _ -> l)
       [] lps in
@@ -239,13 +235,6 @@ let pr_cs_pattern = function
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
 
-let warn_redundant_canonical_projection =
-  CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
-         (fun (hd_val,prj,new_can_s,old_can_s) ->
-          strbrk "Ignoring canonical projection to " ++ hd_val
-          ++ strbrk " by " ++ prj ++ strbrk " in "
-          ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
-
 let open_canonical_structure i (_,o) =
   if Int.equal i 1 then
     let lo = compute_canonical_projections o in
@@ -256,12 +245,14 @@ let open_canonical_structure i (_,o) =
       in match ocs with
         | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
+            if Flags.is_verbose () then
               let old_can_s = (Termops.print_constr cs.o_DEF)
               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
-              warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
-          lo
+              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
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ee55915211..13b5848a33 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -29,15 +29,10 @@ let cbv_vm env sigma c =
     error "vm_compute does not support existential variables.";
   Vnorm.cbv_vm env c ctyp
 
-let warn_native_compute_disabled =
-  CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
-  (fun () ->
-   strbrk "native_compute disabled at configure time; falling back to vm_compute.")
-
 let cbv_native env sigma c =
   if Coq_config.no_native_compiler then
-    (warn_native_compute_disabled ();
-     cbv_vm env sigma c)
+    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
     Nativenorm.native_norm env sigma c ctyp
@@ -214,11 +209,6 @@ let contextualize f g = function
       e_red (contextually b (l,c) (fun _ -> h))
   | None -> e_red g
 
-let warn_simpl_unfolding_modifiers =
-  CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
-         (fun () ->
-          Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
-
 let reduction_of_red_expr env =
   let make_flag = make_flag env in
   let rec reduction_of_red_expr = function
@@ -231,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
-	 warn_simpl_unfolding_modifiers () 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/stm/lemmas.ml b/stm/lemmas.ml
index 50dceb8e6b..a2e8fac059 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -301,16 +301,13 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
 
 (* Admitted *)
 
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
-                                spc () ++ strbrk "declared as an axiom.")
-
 let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
+  | Local, _, _ | Discharge, _, _ ->
+    Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+      str "declared as an axiom.")
   in
   let () = assumption_message id in
   Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
diff --git a/stm/stm.ml b/stm/stm.ml
index 3fb3a2f321..d460cea943 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,6 +989,8 @@ end = struct (* {{{ *)
       | VernacResetInitial ->
           VtStm (VtBack Stateid.initial, true), VtNow
       | VernacResetName (_,name) ->
+          msg_warning
+            (str"Reset not implemented for automatically generated constants");
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
             let oid =
@@ -1038,8 +1040,8 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       Errors.errorlabstrm "undo_vernac_classifier"
-        (str "Cannot undo")
+       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
+       VtStm (VtBack Stateid.initial, true), VtNow
 
 end (* }}} *)
 
@@ -1366,7 +1368,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_debug (str "STM: sending back a fat state");
+          msg_warning (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -1896,12 +1898,6 @@ let delegate name =
   || !Flags.compilation_mode = Flags.BuildVio
   || !Flags.async_proofs_full
  
-let warn_deprecated_nested_proofs =
-  CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
-         (fun () ->
-          strbrk ("Nested proofs are deprecated and will "^
-                    "stop working in a future Coq version"))
-
 let collect_proof keep cur hd brkind id =
  prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
@@ -1966,7 +1962,8 @@ let collect_proof keep cur hd brkind id =
         let name = name ids in
         `MaybeASync (parent last, None, accn, name, delegate name)
     | `Sideff _ ->
-       warn_deprecated_nested_proofs ();
+        Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^
+           "stop working in the next Coq version")));
         `Sync (no_name,None,`NestedProof)
     | _ -> `Sync (no_name,None,`Unknown) in
  let make_sync why = function
@@ -2413,7 +2410,10 @@ let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
-  ({ verbose; loc; expr } as x) c =
+  ({ verbose; loc; expr } as x) c
+ =
+  let warn_if_pos a b =
+    if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
   prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
@@ -2427,12 +2427,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
       | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
       (* Joining various parts of the document *)
-      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
-      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
-      | VtStm (VtWait, b),     VtNow -> finish (); wait (); `Ok
+      | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> warn_if_pos x b; finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> warn_if_pos x b; finish (); wait (); `Ok
       | VtStm (VtPrintDag, b), VtNow ->
-          VCS.print ~now:true (); `Ok
-      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
+          warn_if_pos x b; VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> warn_if_pos x b; observe id; `Ok
       | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
                 |VtPrintDag |VtWait),_), VtLater ->
           anomaly(str"classifier: join actions cannot be classified as VtLater")
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2c2b76412f..9527191299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -708,7 +708,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
-	    Feedback.msg_info (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);
@@ -743,12 +743,6 @@ let input_context_set : Univ.ContextSet.t -> Libobject.obj =
       discharge_function = (fun (_,a) -> Some a);
       classify_function = (fun a -> Keep a) }
 
-let warn_polymorphic_hint =
-  CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
-         (fun hint -> strbrk"Using polymorphic hint " ++ hint ++
-                        str" monomorphically" ++
-                        strbrk" use Polymorphic Hint to use it polymorphically.")
-
 let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
@@ -760,7 +754,9 @@ let fresh_global_or_constr env sigma poly cr =
     else if Univ.ContextSet.is_empty ctx then (c, ctx)
     else begin
       if isgr then
-        warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
+        Feedback.msg_warning (str"Using polymorphic hint " ++
+		     pr_hint_term env sigma ctx cr ++ str" monomorphically" ++
+		     str" use Polymorphic Hint to use it polymorphically.");
       Lib.add_anonymous_leaf (input_context_set ctx);
       (c, Univ.ContextSet.empty)
     end
@@ -1393,15 +1389,10 @@ let print_mp mp =
 
 let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
 
-let warn_non_imported_hint =
-  CWarnings.create ~name:"non-imported-hint" ~category:"automation"
-         (fun (hint,mp) ->
-          strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
-
 let warn h x =
   let hint = pr_hint h in
   let (mp, _, _) = KerName.repr h.uid in
-  warn_non_imported_hint (hint,mp);
+  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 cf842d6f19..f3e117f8c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2976,17 +2976,13 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
  *)
 
-let warn_unused_intro_pattern =
-  CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
-         (fun names ->
-          strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-          ++ str": " ++ prlist_with_sep spc 
-         (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
-
 let check_unused_names names =
   if not (List.is_empty names) && Flags.is_verbose () then
-    warn_unused_intro_pattern names
+    Feedback.msg_warning
+      (str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
+       ++ str": " ++ prlist_with_sep spc 
+	 (Miscprint.pr_intro_pattern 
+	    (fun c -> Printer.pr_constr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
 
 let intropattern_of_name gl avoid = function
   | Anonymous -> IntroNaming IntroAnonymous
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index e45ab4b4e1..0bb7966d72 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -13,6 +13,13 @@ open Type_errors
 open Pretype_errors
 open Indrec
 
+let print_loc loc =
+  if Loc.is_ghost loc then
+    (str"<unknown>")
+  else
+    let loc = Loc.unloc loc in
+    (int (fst loc) ++ str"-" ++ int (snd loc))
+
 let guill s = str "\"" ++ str s ++ str "\""
 
 (** Invariant : exceptions embedded in EvaluatedError satisfy
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index a67c887af3..cd6ccd5653 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -9,6 +9,10 @@
 (** Toplevel Exception *)
 exception EvaluatedError of Pp.std_ppcmds * exn option
 
+(** Error report. *)
+
+val print_loc : Loc.t -> Pp.std_ppcmds
+
 (** Pre-explain a vernac interpretation error *)
 
 val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn
diff --git a/toplevel/class.ml b/toplevel/class.ml
index fa68a69fb1..10e9b30bee 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -32,6 +32,7 @@ type coercion_error_kind =
   | NotAFunction
   | NoSource of cl_typ option
   | ForbiddenSourceClass of cl_typ
+  | NotUniform
   | NoTarget
   | WrongTarget of cl_typ * cl_typ
   | NotAClass of global_reference
@@ -50,6 +51,9 @@ let explain_coercion_error g = function
       (str ": cannot find the source class of " ++ Printer.pr_global g)
   | ForbiddenSourceClass cl ->
       pr_class cl ++ str " cannot be a source class"
+  | NotUniform ->
+      (Printer.pr_global g ++
+         str" does not respect the uniform inheritance condition");
   | NoTarget ->
       (str"Cannot find the target class")
   | WrongTarget (clt,cl) ->
@@ -243,12 +247,6 @@ booleen "coercion identite'?"
 lorque source est None alors target est None aussi.
 *)
 
-let warn_uniform_inheritance =
-  CWarnings.create ~name:"uniform-inheritance" ~category:"typechecker"
-         (fun g ->
-          Printer.pr_global g ++
-            strbrk" does not respect the uniform inheritance condition")
-
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
   let t = Global.type_of_global_unsafe coef in
@@ -264,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
-    warn_uniform_inheritance coef;
+    Feedback.msg_warning (explain_coercion_error coef NotUniform);
   let clt =
     try
       get_target tg ind
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ffa2484eef..28fa8a171b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -82,12 +82,6 @@ let red_constant_entry n ce sigma = function
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
 
-let warn_implicits_in_term =
-  CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
-         (fun () ->
-          strbrk "Implicit arguments declaration relies on type." ++ spc () ++
-            strbrk "The term declares more implicits than the type here.")
-        
 let interp_definition pl bl p red_option c ctypopt =
   let env = Global.env() in
   let ctx = Evd.make_evar_universe_context env pl in
@@ -125,7 +119,9 @@ 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 warn_implicits_in_term ();
+	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) 
           (Universes.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
@@ -140,15 +136,11 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
   ce
 
-let warn_local_let_definition =
-  CWarnings.create ~name:"local-let-definition" ~category:"scope"
-         (fun id ->
-          pr_id id ++ strbrk " is declared as a local definition")
-
 let get_locality id = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
-   warn_local_let_definition id;
+  let msg = pr_id id ++ strbrk " is declared as a local definition" in
+  let () = Feedback.msg_warning msg in
   true
 | Local -> true
 | Global -> false
@@ -166,12 +158,6 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let warn_definition_not_visible =
-  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
-         (fun ident ->
-          strbrk "Section definition " ++
-            pr_id ident ++ strbrk " is not visible from current goals")
-
 let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
@@ -183,7 +169,9 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
     let () = if Pfedit.refining () then
-	       warn_definition_not_visible ident
+      let msg = strbrk "Section definition " ++
+        pr_id ident ++ strbrk " is not visible from current goals" in
+      Feedback.msg_warning msg
     in
     gr
   | Discharge | Local | Global ->
@@ -229,7 +217,7 @@ match local with
   let () = assumption_message ident in
   let () =
     if is_verbose () && Pfedit.refining () then
-    Feedback.msg_info (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
@@ -792,25 +780,20 @@ let rec partial_order cmp = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if Id.List.mem x yge then
-      pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely"
+      pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely"
     else if Id.List.mem y xge then
-      pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely"
+      pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely"
     else
-      pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in
-  let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
+      pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in
+  let e = if List.is_empty rest then reason else str "e.g., " ++ reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
     if isfix
-    then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
+    then str "Well-foundedness check may fail unexpectedly." ++ fnl()
     else mt () in
-  strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++
+  str "Not a fully mutually defined " ++ str k ++ fnl () ++
   str "(" ++ e ++ str ")." ++ fnl () ++ w
 
-let warn_non_full_mutual =
-  CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints"
-         (fun (x,xge,y,yge,isfix,rest) ->
-          non_full_mutual_message x xge y yge isfix rest)
-
 let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
   let preorder =
@@ -820,7 +803,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 ->
-       warn_non_full_mutual (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 50a2280502..65c5917b72 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -135,7 +135,6 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    Errors.errorlabstrm "get_compat_version"
-      (str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s -> Errors.errorlabstrm "get_compat_version"
-      (str "Unknown compatibility version \"" ++ str s ++ str "\".")
+    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 191c937d7d..00e0219f1d 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -146,8 +146,9 @@ let print_highlight_location ib loc =
                       str sn ++ str dn) in
 	  (l1 ++ li ++ ln)
   in
-  let loc  = Loc.make_loc (bp,ep) in
-  (Pp.pr_loc loc ++ highlight_lines ++ fnl ())
+  let loc = Loc.make_loc (bp,ep) in
+  (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++
+     highlight_lines ++ fnl ())
 
 (* Functions to report located errors in a file. *)
 
@@ -162,7 +163,10 @@ let print_location_in_file loc =
     in
     let open Loc in
     hov 0 (* No line break so as to follow emacs error message format *)
-	(errstrm ++ Pp.pr_loc loc)
+	(errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   Cerrors.print_loc (Loc.make_loc (loc.bp-loc.bol_pos,loc.ep-loc.bol_pos))) ++ str":" ++
+      fnl ()
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
@@ -245,7 +249,7 @@ let print_toplevel_error (e, info) =
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   let fname = loc.Loc.fname in
   let locmsg =
-    if Loc.is_ghost loc || String.equal fname "" then
+    if String.equal fname "" then
       if locate_exn e && valid_buffer_loc top_buffer loc then
 	print_highlight_location top_buffer loc
       else mt ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 93ed2481b1..e34f38eb37 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -123,6 +123,16 @@ let engage () =
 
 let set_batch_mode () = batch_mode := true
 
+let user_warning = ref false
+(** User explicitly set warning *)
+
+let set_warning p =
+  let () = user_warning := true in
+  match p with
+  | "all" -> make_warn true
+  | "none" -> make_warn false
+  | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+
 let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
@@ -132,27 +142,18 @@ let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
-let warn_deprecated_inputstate =
-  CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
-         (fun () -> strbrk "The inputstate option is deprecated and discouraged.")
-
 let inputstate = ref ""
 let set_inputstate s =
-  warn_deprecated_inputstate ();
+  let () = Feedback.msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
 let inputstate () =
   if not (String.is_empty !inputstate) then
     let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
     intern_state fname
 
-let warn_deprecated_outputstate =
-  CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
-         (fun () ->
-          strbrk "The outputstate option is deprecated and discouraged.")
-
 let outputstate = ref ""
 let set_outputstate s =
-  warn_deprecated_outputstate ();
+  let () = Feedback.msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
 let outputstate () =
   if not (String.is_empty !outputstate) then
@@ -531,7 +532,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> set_toploop (next ())
-    |"-w" | "-W" -> CWarnings.set_flags (next ())
+    |"-w" -> set_warning (next ())
     |"-o" -> Flags.compilation_output_name := Some (next())
 
     (* Options with zero arg *)
@@ -639,7 +640,7 @@ let init_toplevel arglist =
       engage ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
-(*       Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *)
+      Syntax_def.set_compat_notations (not !no_compat_ntn);
       if (not !batch_mode || List.is_empty !compile_list)
          && Global.env_is_initial ()
       then Option.iter Declaremods.start_library !toplevel_name;
@@ -676,6 +677,7 @@ let start () =
   let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
   (* In batch mode, Coqtop has already exited at this point. In interactive one,
      dump glob is nothing but garbage ...  *)
+  if not !user_warning then make_warn true;
   !toploop_run ();
   exit 1
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index bbee39c3d6..a48bbf89d9 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -150,7 +150,7 @@ let alarm what internal msg =
   | UserAutomaticRequest
   | InternalTacticRequest ->
     (if debug then
-      Feedback.msg_debug
+      Feedback.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
   | _ -> Some msg
 
@@ -295,11 +295,6 @@ let declare_rewriting_schemes ind =
       (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind
   end
 
-let warn_cannot_build_congruence =
-  CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes"
-         (fun () ->
-          strbrk "Cannot build congruence scheme because eq is not found")
-
 let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
@@ -308,7 +303,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
-      warn_cannot_build_congruence ()
+      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 62aa85160c..c4c891b89c 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -26,11 +26,6 @@ let check_locality locality_flag =
 
 (* Commands which supported an inlined Local flag *)
 
-let warn_deprecated_local_syntax =
-  CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated"
-         (fun () ->
-          Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.")
-
 let enforce_locality_full locality_flag local =
   let local =
     match locality_flag with
@@ -40,8 +35,8 @@ let enforce_locality_full locality_flag local =
 	Errors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
-	    warn_deprecated_local_syntax ();
-	    Some true
+          Feedback.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix.");
+	  Some true
 	end else
 	None
     | Some b -> Some b in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index aa6601a7d2..e772ea0205 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -864,23 +864,16 @@ let check_rule_productivity l =
   if (match l with SProdList _ :: _ -> true | _ -> false) then
     error "A recursive notation must start with at least one symbol."
 
-let warn_notation_bound_to_variable =
-  CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
-         (fun () ->
-          strbrk "This notation will not be used for printing as it is bound to a single variable.")
-
-let warn_non_reversible_notation =
-  CWarnings.create ~name:"non-reversible-notation" ~category:"parsing"
-         (fun () ->
-          strbrk "This notation will not be used for printing as it is not reversible.")
-
 let is_not_printable onlyparse noninjective = function
 | NVar _ ->
-  if not onlyparse then warn_notation_bound_to_variable ();
+  let () = if not onlyparse then
+    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
-     (warn_non_reversible_notation (); true)
+  if not onlyparse && noninjective then
+    let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
+    true
   else onlyparse
 
 let find_precedence lev etyps symbols =
@@ -935,10 +928,6 @@ let check_curly_brackets_notation_exists () =
     error "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved."
 
-let warn_skip_spaces_curly =
-  CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing"
-      (fun () ->strbrk "Skipping spaces inside curly brackets")
-
 (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
 let remove_curly_brackets l =
   let rec skip_break acc = function
@@ -953,10 +942,9 @@ let remove_curly_brackets l =
             let br',next' = skip_break [] l' in
             (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
-		  warn_skip_spaces_curly ();
-		  if deb && List.is_empty l'' then [t1;x;t2] else begin
+                  if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
+                    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''
                   end
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index acd8026f92..36c16208c5 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -146,12 +146,7 @@ let dir_ml_load s =
 let dir_ml_use s =
   match !load with
     | WithTop t -> t.use_file s
-    | _ ->
-       let moreinfo =
-	 if Dynlink.is_native then " Loading ML code works only in bytecode."
-	 else ""
-       in
-      errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+    | _ -> Feedback.msg_warning (str "Cannot access the ML compiler")
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
@@ -166,22 +161,12 @@ let add_rec_ml_dir unix_path =
 
 (* Adding files to Coq and ML loadpath *)
 
-let warn_cannot_use_directory =
-  CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem"
-         (fun d ->
-          str "Directory " ++ str d ++
-            strbrk " cannot be used as a Coq identifier (skipped)")
-
 let convert_string d =
   try Names.Id.of_string d
   with UserError _ ->
-    warn_cannot_use_directory d;
+    Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
-let warn_cannot_open_path =
-  CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
-      (fun unix_path -> str "Cannot open " ++ str unix_path)
-
 let add_rec_path ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
@@ -199,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
-    warn_cannot_open_path 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 =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3151b13726..fe6ed55a7b 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -173,13 +173,6 @@ type record_error =
   | MissingProj of Id.t * Id.t list
   | BadTypedProj of Id.t * env * Type_errors.type_error
 
-let warn_cannot_define_projection =
-  CWarnings.create ~name:"cannot-define-projection" ~category:"records"
-         (fun msg -> hov 0 msg)
-
-(* If a projection is not definable, we throw an error if the user
-asked it to be a coercion. Otherwise, we just print an info
-message. The user might still want to name the field of the record. *)
 let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
@@ -204,7 +197,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 Feedback.msg_info (hov 0 st)
+  Flags.if_verbose Feedback.msg_warning (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
@@ -247,12 +240,6 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
   let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
   Termops.substl_rel_context (subst@[mkIndU indu]) fields
 
-let warn_non_primitive_record =
-  CWarnings.create ~name:"non-primitive-record" ~category:"record"
-         (fun (env,indsp) ->
-          (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
-                    strbrk" could not be defined as a primitive record")))
-
 (* We build projections *)
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
@@ -276,7 +263,9 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	| Some None | None -> false
       in
 	if not is_primitive then 
-	  warn_non_primitive_record (env,indsp);
+	  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
     else false
   in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 972d83055a..ac9293d5f8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -18,15 +18,14 @@ open Vernacexpr
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-(* Navigation commands are allowed in a coqtop session but not in a .v file *)
+(* The navigation vernac commands will be handled separately *)
 
 let rec is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
-  | VernacBack _
-  | VernacStm _ -> true
+  | VernacBack _ -> true
   | VernacRedirect (_, (_,c))
   | VernacTime (_,c) ->
       is_navigation_vernac c (* Time Back* is harmless *)
@@ -231,7 +230,6 @@ 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
-      CWarnings.set_current_loc (fst loc_ast);
       vernac_com verbosely checknav loc_ast
     done
   with any ->   (* whatever the exception *)
@@ -274,17 +272,11 @@ let load_vernac verb file =
     if !Flags.beautify_file then close_out !chan_beautify;
     iraise (disable_drop e, info)
 
-let warn_file_no_extension =
-  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
-         (fun (f,ext) ->
-          str "File \"" ++ str f ++
-            strbrk "\" has been implicitly expanded to \"" ++
-            str f ++ str ext ++ str "\"")
-
 let ensure_ext ext f =
   if Filename.check_suffix f ext then f
   else begin
-    warn_file_no_extension (f,ext);
+    Feedback.msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    expanded to \"" ++ str f ++ str ext ++ str "\"");
     f ^ ext
   end
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 65aa46bc16..82fe9751eb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -896,11 +896,7 @@ let vernac_chdir = function
   | Some path ->
       begin
 	try Sys.chdir (expand path)
-	with Sys_error err ->
-	  (* Cd is typically used to control the output directory of
-	  extraction. A failed Cd could lead to overwriting .ml files
-	  so we make it an error. *)
-	  Errors.error ("Cd failed: " ^ err)
+	with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err)
       end;
       if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
@@ -947,16 +943,6 @@ let vernac_declare_implicits locality r l =
       Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
-let warn_arguments_assert =
-  CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
-         (fun sr ->
-          strbrk "This command is just asserting the number and names of arguments of " ++
-            pr_global sr ++ strbrk". If this is what you want add " ++
-            strbrk "': assert' to silence the warning. If you want " ++
-            strbrk "to clear implicit arguments add ': clear implicits'. " ++
-            strbrk "If you want to clear notation scopes add ': clear scopes'")
-         
-
 let vernac_declare_arguments locality r l nargs flags =
   let extra_scope_flag = List.mem `ExtraScopes flags in
   let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
@@ -1085,7 +1071,7 @@ let vernac_declare_arguments locality r l nargs flags =
           some_scopes_specified ||
           some_simpl_flags_specified) &&
      no_flags then
-    warn_arguments_assert sr
+    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 () = {
@@ -1356,15 +1342,6 @@ let _ =
       optread  = (fun () -> !Constrintern.parsing_explicit);
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
-let _ =
-  declare_string_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "warnings display";
-      optkey   = ["Warnings"];
-      optread  = CWarnings.get_flags;
-      optwrite = CWarnings.set_flags }
-
 let vernac_set_strategy locality l =
   let local = make_locality locality in
   let glob_ref r =
@@ -1878,12 +1855,12 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> Errors.errorlabstrm "" (str "Abort cannot be used through the Load command")
-  | VernacAbortAll -> Errors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
-  | VernacRestart -> Errors.errorlabstrm "" (str "Restart cannot be used through the Load command")
-  | VernacUndo _ -> Errors.errorlabstrm "" (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _ -> Errors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
-  | VernacBacktrack _ -> Errors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
+  | 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
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 0abc9e76d0..1116a31046 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -42,11 +42,6 @@ let vinterp_map s =
 
 let vinterp_init () = Hashtbl.clear vernac_tab
 
-let warn_deprecated_command =
-  let open CWarnings in
-  create ~name:"deprecated-command" ~category:"deprecated"
-         (fun pr -> str "Deprecated vernacular command: " ++ pr)
-
 (* Interpretation of a vernac command *)
 
 let call ?locality (opn,converted_args) =
@@ -60,7 +55,7 @@ let call ?locality (opn,converted_args) =
       | Egramml.GramNonTerminal _ -> str "_"
       in
       let pr = pr_sequence pr_gram rules in
-      warn_deprecated_command pr;
+      Feedback.msg_warning (str "Deprecated vernacular command: " ++ pr)
     in
     loc:= "Checking arguments";
     let hunk = callback converted_args in