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/nativevalues.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/nativevalues.mli')

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 983e7588d6..79e35d4a04 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -41,8 +41,8 @@ val eq_rec_pos : rec_pos -> rec_pos -> bool
 
 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) 
@@ -59,9 +59,9 @@ type atom =
 val mk_accu : atom -> t
 val mk_rel_accu : int -> t
 val mk_rels_accu : int -> int -> t array
-val mk_constant_accu : constant -> t
-val mk_ind_accu : inductive -> t
-val mk_sort_accu : sorts -> t
+val mk_constant_accu : constant -> Univ.Level.t array -> t
+val mk_ind_accu : inductive -> Univ.Level.t array -> t
+val mk_sort_accu : sorts -> Univ.Level.t array -> t
 val mk_var_accu : identifier -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
 val mk_prod_accu : name -> t -> t -> t
-- 
cgit v1.2.3