diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b09367dd92..68783780d3 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -738,14 +738,9 @@ let vm_conv cv_pb env t1 t2 = (* If compilation fails, fall-back to closure 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)) - -let set_default_conv f = default_conv := f - let default_conv cv_pb ?(l2r=false) env t1 t2 = try - !default_conv ~l2r cv_pb env t1 t2 + fconv cv_pb l2r (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 |