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