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/vconv.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/vconv.ml')

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