diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 13:50:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 13:50:55 +0200 |
| commit | 0f74b3df6e64dc069e53c4afcd6f46129b211d09 (patch) | |
| tree | 5b34bda641bc8454b88ad6659f68f6b4621e1302 | |
| parent | f45a88ad054b88792ec8cc6631e4d4015fa95bab (diff) | |
Remove reference to default conversion function inside the kernel.
| -rw-r--r-- | kernel/reduction.ml | 7 | ||||
| -rw-r--r-- | kernel/reduction.mli | 1 |
2 files changed, 1 insertions, 7 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b09367dd9..68783780d 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 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6ced5c498..90c008b19 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -93,7 +93,6 @@ val set_nat_conv : (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function -val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function |