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, 32 insertions, 23 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 893baad8c9..93a89330e3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -198,15 +198,13 @@ let warning_error names e =
   let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-	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 ())
+       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)
     | Defining_principle e ->
-	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 ())
+       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)
     | _ -> raise e
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1c5eb16218..2ebbb34e4c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -227,6 +227,11 @@ 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 
@@ -269,14 +274,20 @@ let derive_inversion fix_names =
 	lind;
       with e when Errors.noncritical e ->
       let e' = process_vernac_interp_error e in
-      Feedback.msg_warning
-	(str "Cannot build inversion information" ++
-	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
+      warn_funind_cannot_build_inversion e'
   with e when Errors.noncritical e ->
-      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 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 warning_error names e =
   let e = process_vernac_interp_error e in
@@ -294,15 +305,11 @@ let warning_error names e =
   in
   match e with
     | Building_graph 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)
+       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+       warn_cannot_define_graph (names,e_explain e)
     | Defining_principle 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)
+       let names = prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names in
+       warn_cannot_define_principle (names,e_explain e)
     | _ -> raise e
 
 let error_error names e =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index e720691406..1c27bdface 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,9 @@
 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 ->