From 0e07e69dae3f3f4a99f824533f54a3991aacac6a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 13:55:20 +0200
Subject: 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.
---
 kernel/reduction.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'kernel/reduction.ml')

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 =
-- 
cgit v1.2.3