diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index acc97380a..9d1d12573 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -54,6 +54,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_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 |