diff options
Diffstat (limited to 'kernel/nativeconv.mli')
| -rw-r--r-- | kernel/nativeconv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 21f0b2e9e..4dddb9fd3 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -15,4 +15,4 @@ val native_conv : conv_pb -> evars -> types conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) -val native_conv_gen : conv_pb -> evars -> (constr, 'a) generic_conversion_function +val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function |