diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /kernel/reduction.ml | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
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 29c6009ce..6e1c3c5b7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -733,14 +733,9 @@ let vm_conv cv_pb 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)) - -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 false (fun _ -> None) env t1 t2 with Not_found | Invalid_argument _ -> Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion"); fconv cv_pb false (fun _->None) env t1 t2 |