diff options
Diffstat (limited to 'kernel/vconv.mli')
| -rw-r--r-- | kernel/vconv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 7e5397c06..ff01735c0 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,7 @@ open Reduction (********************************************************************** s conversion functions *) -val vm_conv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) |