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, 7 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 30a346c910..710bfa19b8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -676,12 +676,18 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
 let vm_conv = ref (fun cv_pb env ->
 		   gen_conv cv_pb env ~evars:((fun _->None), universes env))
 
+let warn_bytecode_compiler_failed =
+  let open Pp in
+  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
+         (fun () -> strbrk "Bytecode compiler failed, " ++
+                      strbrk "falling back to standard conversion")
+
 let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    warn_bytecode_compiler_failed ();
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =