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.

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e2a19b0e8..7d64e894d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -303,6 +303,10 @@ module Level = struct
   let var n = 
     if n < 20 then vars.(n) else make (Var n)
 
+  let var_index u =
+    match data u with
+    | Var n -> Some n | _ -> None
+
   let make m n = make (Level (n, Names.DirPath.hcons m))
 
 end