aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/reduction.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 9479e38ca..0f105b048 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -735,8 +735,9 @@ 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 default conversion");
+ fconv cv_pb false (fun _->None) env t1 t2)
let default_conv cv_pb ?(l2r=false) env t1 t2 =
fconv cv_pb false (fun _ -> None) env t1 t2