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

2 files changed, 5 insertions, 23 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index ac6a7ac7f..2ec6430fd 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -111,14 +111,8 @@ 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
-      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)) ]; } >>
+      Tacenv.register_ml_tactic $se$ [|$tac$|];
+      Mltop.declare_cache_obj obj $plugin_name$; } >>
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
@@ -129,14 +123,8 @@ 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$; }
-      with [ e when Errors.noncritical e ->
-        Feedback.msg_warning
-          (Pp.app
-            (Pp.str ("Exception in tactic extend " ^ $entry$ ^": "))
-            (Errors.print e)) ]; } >>
+        Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
     ]
 
 open Pcaml
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index ce0431889..04b117fba 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -122,14 +122,8 @@ 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 {
-	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 (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
+        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
 	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
       } >> ]