diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 17:17:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:36:30 +0200 |
| commit | 7ae876ab6246a9c9d352b7c72d3f98db47ff456c (patch) | |
| tree | 70063072734746156cc59277078df125d2f2f1aa /kernel/reduction.ml | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Remove now useless exception handler in default conversion.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ccea06c76..9479e38ca 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -739,11 +739,7 @@ let vm_conv cv_pb env t1 t2 = fconv cv_pb false (fun _->None) env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = - try fconv cv_pb false (fun _ -> None) 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 let default_conv_leq = default_conv CUMUL (* |