aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-14 17:23:27 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-10-15 14:36:30 +0200
commitd08aa6b4f742a7162e726920810765258802c176 (patch)
treee1cca6b452cdbebb79d0ef9d4bd45693ccfd1bbd /kernel/reduction.ml
parent7ae876ab6246a9c9d352b7c72d3f98db47ff456c (diff)
Warn user when bytecode compilation fails.
Previously, the kernel was silently switching back to the standard conversion.
Diffstat (limited to 'kernel/reduction.ml')
-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