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, 6 insertions, 33 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index b12d2038a..3e08b38b1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -12,18 +12,6 @@ open Util
 
 module Dyn = Dyn.Make(struct end)
 
-(* The relax flag is used to make it possible to load files while ignoring
-   failures to incorporate some objects.  This can be useful when one
-   wants to work with restricted Coq programs that have only parts of
-   the full capabilities, but may still be able to work correctly for
-   limited purposes.  One example is for the graphical interface, that uses
-   such a limited Coq process to do only parsing.  It loads .vo files, but
-   is only interested in loading the grammar rule definitions. *)
-
-let relax_flag = ref false;;
-
-let relax b = relax_flag := b;;
-
 type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
@@ -114,31 +102,16 @@ let declare_object_full odecl =
   try declare_object_full odecl
   with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
 
-let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
-
 (* this function describes how the cache, load, open, and export functions
-   are triggered.  In relaxed mode, this function just return a meaningless
-   value instead of raising an exception when they fail. *)
+   are triggered. *)
 
 let apply_dyn_fun deflt f lobj =
   let tag = object_tag lobj in
-  try
-    let dodecl =
-      try
-        Hashtbl.find cache_tab tag
-      with Not_found ->
-        failwith "local to_apply_dyn_fun" in
-    f dodecl
-  with
-    Failure "local to_apply_dyn_fun" ->
-      if not (!relax_flag || Hashtbl.mem missing_tab tag) then
-        begin
-          Feedback.msg_warning
-	    (Pp.str ("Cannot find library functions for an object with tag "
-                      ^ tag ^ " (a plugin may be missing)"));
-          Hashtbl.add missing_tab tag ()
-        end;
-      deflt
+  let dodecl =
+    try Hashtbl.find cache_tab tag
+    with Not_found -> assert false
+  in
+  f dodecl
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj