From 4a7d2a7d09c854f7a2060fa40d3dbe5ce033171e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Sep 2015 23:40:52 +0200
Subject: Output a warning when conversion compilation failed.

Previously, the kernel would silently fall back to standard conversion.
---
 kernel/reduction.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b09367dd92..3253cddf7c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -735,8 +735,8 @@ let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-      (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb false (fun _->None) env t1 t2
+    Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    fconv cv_pb false (fun _->None) env t1 t2
 
 
 let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
@@ -747,8 +747,8 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 =
   try
     !default_conv ~l2r cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-      (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb false (fun _->None) env t1 t2
+    Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion");
+    fconv cv_pb false (fun _->None) env t1 t2
 
 let default_conv_leq = default_conv CUMUL
 (*
-- 
cgit v1.2.3