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

8 files changed, 45 insertions, 27 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 55220f44c0..d3d4201f57 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && is_verbose () then
-    Feedback.msg_warning (message_ambig !ambig_paths)
+    Feedback.msg_info (message_ambig !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 129725c6d2..c566839e85 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
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 86921c49b0..cc178eb975 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t =
         share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
-        if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
+        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
         let c = detype flags avoid env sigma c in
         let t = detype flags avoid env sigma t in
         (List.rev l,c,t)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 04100c8a73..5c8060996a 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -334,10 +334,14 @@ let glob_visible_short_qualid c =
         fold_glob_constr aux acc c
   in aux [] c
 
+let warn_variable_collision =
+  let open Pp in
+  CWarnings.create ~name:"variable-collision" ~category:"ltac"
+         (fun name ->
+          strbrk "Collision between bound variables of name " ++ pr_id name)
+
 let add_and_check_ident id set =
-  if Id.Set.mem id set then
-    Feedback.msg_warning
-      Pp.(str "Collision between bound variables of name " ++ Id.print id);
+  if Id.Set.mem id set then warn_variable_collision id;
   Id.Set.add id set
 
 let bound_glob_vars =
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index e0a2de0326..c2b27ca6ab 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -34,6 +34,8 @@ val map_glob_constr :
 val map_glob_constr_left_to_right :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
 
+val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
+
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5d36fc78ef..fc38e98c63 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -183,9 +183,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
               | ra::rest ->
                   (match dest_recarg ra with
 	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
-	            | Imbr _  ->
-		        Feedback.msg_warning (strbrk "Ignoring recursive call");
-		        (None,rest)
+	            | Imbr _  -> (None,rest)
                     | _ -> (None, rest))
 	  in
           (match optionpos with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d6305d81a8..7eb3d633da 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -317,6 +317,10 @@ let rev_it_mkPLambda = List.fold_right mkPLambda
 
 let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
 
+let warn_cast_in_pattern =
+  CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
+    (fun () -> Pp.strbrk "Casts are ignored in patterns")
+
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
       (try PRel (List.index Name.equal (Name id) vars)
@@ -348,7 +352,7 @@ let rec pat_of_raw metas vars = function
   | GHole _ ->
       PMeta None
   | GCast (_,c,_) ->
-      Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern");
+      warn_cast_in_pattern ();
       pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bbb6a92663..2959bd7c84 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -187,6 +187,13 @@ let cs_pattern_of_constr t =
           with e when Errors.noncritical e -> raise Not_found
 	end
 
+let warn_projection_no_head_constant =
+  CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
+         (fun (t,con_pp,proji_sp_pp) ->
+          strbrk "Projection value has no head constant: "
+          ++ Termops.print_constr t ++ strbrk " in canonical instance "  
+          ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
+
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
@@ -213,13 +220,10 @@ let compute_canonical_projections (con,ind) =
 		   let patt, n , args = cs_pattern_of_constr t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
-                   if Flags.is_verbose () then
-                     (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
+                     let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-		      Feedback.msg_warning (strbrk "No global reference exists for projection value"
-                                   ++ Termops.print_constr t ++ strbrk " in instance "  
-                                   ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
-		   l
+                     warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
+                   l
 	       end
 	   | _ -> l)
       [] lps in
@@ -235,6 +239,13 @@ let pr_cs_pattern = function
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
 
+let warn_redundant_canonical_projection =
+  CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
+         (fun (hd_val,prj,new_can_s,old_can_s) ->
+          strbrk "Ignoring canonical projection to " ++ hd_val
+          ++ strbrk " by " ++ prj ++ strbrk " in "
+          ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
+
 let open_canonical_structure i (_,o) =
   if Int.equal i 1 then
     let lo = compute_canonical_projections o in
@@ -245,14 +256,12 @@ let open_canonical_structure i (_,o) =
       in match ocs with
         | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
-            if Flags.is_verbose () then
               let old_can_s = (Termops.print_constr cs.o_DEF)
               and new_can_s = (Termops.print_constr s.o_DEF) in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
-              Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
-                             ++ strbrk " by " ++ prj ++ strbrk " in "
-                             ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo
+              warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
+          lo
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o