A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args

3 files changed, 74 insertions, 59 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a03be5743f..94981d0e1f 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_both_mod_and_cst q mp r;
-	    let refs,mps = locate_ref l in refs,mp::mps
+           warning_ambiguous_name (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 560fe5aea8..81dfa603dd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -295,81 +295,94 @@ 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 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;
+  if not (List.is_empty info_axioms) then
+    warn_extraction_axiom_to_realize info_axioms;
   let log_axioms = Refset'.elements !log_axioms in
-  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
+  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 ())
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if List.is_empty opaques then ()
-  else
+  if not (List.is_empty opaques) then
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
-    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 ())
+    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 ())
 
 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
-    Feedback.msg_warning
-      (str "Extraction inside an opened module is experimental.\n" ++
-       str "In case of problem, close it first.\n")
+    warn_extraction_inside_module ()
 
 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 warning_id s =
-  Feedback.msg_warning (str ("The identifier "^s^
-		    " contains __ which is reserved for the extraction"))
+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 error_constant r =
   err (safe_pr_global r ++ str " is not a constant.")
@@ -447,12 +460,15 @@ 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
-  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.")
+  warn_extraction_remaining_implicit s
 
 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 62c20bd3a7..15a08756c0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_both_mod_and_cst :
- qualid -> module_path -> global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> 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