Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

6 files changed, 15 insertions, 34 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8cbc3ab445..a0ef5e570e 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,8 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else
-	       (fun x -> Feedback.msg_warning x) in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 2f985e15ac..a0ff9e123a 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -145,16 +145,11 @@ let native_conv_gen pb sigma env univs t1 t2 =
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
-let warn_no_native_compiler =
-  let open Pp in
-  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
-         (fun () -> strbrk "Native compiler is disabled," ++
-                      strbrk " falling back to VM conversion test.")
-
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
-    warn_no_native_compiler ();
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
+    Feedback.msg_warning (Pp.str msg);
     vm_conv cv_pb env t1 t2
   end
   else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d4a67b3999..5b92e9554f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -55,15 +55,6 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
-let warn_native_compiler_failed =
-  let print = function
-  | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
-  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
-  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
-  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
-  in
-  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
-
 let call_compiler ml_filename =
   let load_path = !get_load_paths () in
   let load_path = List.map (fun dn -> dn / output_dir) load_path in
@@ -87,12 +78,15 @@ let call_compiler ml_filename =
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        warn_native_compiler_failed (Inl res); false
-    in
+      | Unix.WEXITED n ->
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
+      | Unix.WSIGNALED n ->
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
+      | Unix.WSTOPPED n ->
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    warn_native_compiler_failed (Inr e);
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 710bfa19b8..30a346c910 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -676,18 +676,12 @@ 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 _ ->
-    warn_bytecode_compiler_failed ();
+    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3896446925..1b5e5e32a3 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -106,5 +106,3 @@ exception NotArity
 
 val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
-
-val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c729a6ce29..53db6f5bee 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,9 +185,10 @@ let vm_conv_gen cv_pb env univs t1 t2 =
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
-    warn_bytecode_compiler_failed ();
-    Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      full_transparent_state env univs t1 t2
+    (Feedback.msg_warning
+      (Pp.str "Bytecode compilation failed, falling back to default conversion");
+     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+			    full_transparent_state env univs t1 t2)
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in