diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-04 23:40:52 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-06 21:26:31 +0200 |
| commit | 4a7d2a7d09c854f7a2060fa40d3dbe5ce033171e (patch) | |
| tree | aa7fa6d99f59017faaa01b6f08c4898f28d56f6f /kernel/reduction.ml | |
| parent | d8b245d688ff64d17acd9e7591daf6d63b4e54f7 (diff) | |
Output a warning when conversion compilation failed.
Previously, the kernel would silently fall back to standard conversion.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b09367dd9..3253cddf7 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 (* |