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.

3 files changed, 59 insertions, 74 deletions

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