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

1 files changed, 9 insertions, 8 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 129725c6d..c566839e8 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -49,12 +49,12 @@ type bound_ident_map = Id.t Id.Map.t
 
 exception PatternMatchingFailure
 
-let warn_bound_meta name =
-  Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++
-    str " and a metavariable of same name.")
+let warn_meta_collision =
+  CWarnings.create ~name:"meta-collision" ~category:"ltac"
+         (fun name ->
+          strbrk "Collision between bound variable " ++ pr_id name ++
+            strbrk " and a metavariable of same name.")
 
-let warn_bound_bound name =
-  Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name)
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
@@ -62,18 +62,19 @@ let constrain n (ids, m as x) (names, terms as subst) =
     if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
-    let () = if Id.Map.mem n names then warn_bound_meta n in
+    let () = if Id.Map.mem n names then warn_meta_collision n in
     (names, Id.Map.add n x terms)
 
 let add_binders na1 na2 binding_vars (names, terms as subst) =
   match na1, na2 with
   | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
     if Id.Map.mem id1 names then
-      let () = warn_bound_bound id1 in
+      let () = Glob_ops.warn_variable_collision id1 in
       (names, terms)
     else
       let names = Id.Map.add id1 id2 names in
-      let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
+      let () = if Id.Map.mem id1 terms then
+        warn_meta_collision id1 in
       (names, terms)
   | _ -> subst