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.

9 files changed, 93 insertions, 130 deletions

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 =