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/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8895bae5da..70f6fd803c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -310,7 +310,7 @@ let judge_of_cast env cj k tj =
       | NATIVEcast ->
 	 let sigma = Nativelambda.empty_evars in
          mkCast (cj.uj_val, k, expected_type),
-         native_conv CUMUL sigma env cj.uj_type expected_type
+         Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type
     in
       { uj_val = c;
 	uj_type = expected_type }
-- 
cgit v1.2.3