From 9f5586d88880cbb98c92edfe9c33c76564f1a19c Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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/nativevalues.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'kernel/nativevalues.ml')

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 098c59e82..d7a219505 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -49,8 +49,8 @@ let eq_rec_pos = Array.equal Int.equal
 
 type atom = 
   | Arel of int
-  | Aconstant of constant
-  | Aind of inductive
+  | Aconstant of pconstant
+  | Aind of pinductive
   | Asort of sorts
   | Avar of identifier
   | Acase of annot_sw * accumulator * t * (t -> t)
@@ -106,14 +106,19 @@ let mk_rels_accu lvl len =
 let napply (f:t) (args: t array) =
   Array.fold_left (fun f a -> f a) f args
 
-let mk_constant_accu kn = 
-  mk_accu (Aconstant kn)
+let mk_constant_accu kn u = 
+  mk_accu (Aconstant (kn,Univ.Instance.of_array u))
 
-let mk_ind_accu s = 
-  mk_accu (Aind s)
+let mk_ind_accu ind u = 
+  mk_accu (Aind (ind,Univ.Instance.of_array u))
 
-let mk_sort_accu s =
-  mk_accu (Asort s)
+let mk_sort_accu s u =
+  match s with
+  | Prop _ -> mk_accu (Asort s)
+  | Type s ->
+     let u = Univ.Instance.of_array u in
+     let s = Univ.subst_instance_universe u s in
+     mk_accu (Asort (Type s))
 
 let mk_var_accu id = 
   mk_accu (Avar id)
-- 
cgit v1.2.3