From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- kernel/vconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vconv.mli') diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 7e5397c0..ff01735c 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. *) -- cgit v1.2.3