From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 8 Oct 2015 18:06:55 +0200
Subject: Fix #4346 1/2: native casts were not inferring universe constraints.

---
 kernel/nativeconv.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/nativeconv.mli')

diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 318a7d830b..21f0b2e9e5 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -12,3 +12,7 @@ open Nativelambda
 (** This module implements the conversion test by compiling to OCaml code *)
 
 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
-- 
cgit v1.2.3


From 44817bf722eacb0379bebc7e435bfafa503d574f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2015 14:21:45 +0200
Subject:  Fix #4346 2/2: VM casts were not inferring universe constraints.

---
 kernel/nativeconv.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativeconv.mli')

diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 21f0b2e9e5..4dddb9fd30 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
-- 
cgit v1.2.3