From 9f5586d88880cbb98c92edfe9c33c76564f1a19c 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/nativecode.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/nativecode.mli')

diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 385c77283b..893db92dd8 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -42,6 +42,8 @@ val get_meta : symbol array -> int -> metavariable
 
 val get_evar : symbol array -> int -> existential
 
+val get_level : symbol array -> int -> Univ.Level.t
+
 val get_symbols_tbl : unit -> symbol array
 
 type code_location_update
-- 
cgit v1.2.3