diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6e4634194..2d117cc96 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -55,8 +55,9 @@ val conv_leq_vecti : val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_nat_conv : (conv_pb -> types conversion_function) -> unit -val native_conv : conv_pb -> types conversion_function +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 |