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, 19 insertions, 10 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bbb6a9266..2959bd7c8 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