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/vconv.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel/vconv.mli')

diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 1a29a4d518..49e5d23e63 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,7 +12,11 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val vconv : conv_pb -> types conversion_function
+val vm_conv : conv_pb -> types conversion_function
 
-val val_of_constr : env -> constr -> values
+(** A conversion function parametrized by a universe comparator. Used outside of
+    the kernel. *)
+val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
 
+(** Precompute a VM value from a constr *)
+val val_of_constr : env -> constr -> values
-- 
cgit v1.2.3