From 6e0b660b1e58502b7da477b9725ae8ee4f5d00ed Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 16 Jan 2015 22:17:03 +0100
Subject: Make native compiler handle universe polymorphic definitions.

One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
---
 kernel/declareops.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d5df24a1a1..48a6098eee 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -260,6 +260,16 @@ let subst_mind_body sub mib =
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private }
 
+let inductive_instance mib =
+  if mib.mind_polymorphic then
+    Univ.UContext.instance mib.mind_universes
+  else Univ.Instance.empty
+
+let inductive_context mib =
+  if mib.mind_polymorphic then 
+    Univ.instantiate_univ_context mib.mind_universes 
+  else Univ.UContext.empty
+
 (** {6 Hash-consing of inductive declarations } *)
 
 let hcons_regular_ind_arity a =
-- 
cgit v1.2.3