From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@cs.harvard.edu>
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 kernel/nativelambda.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 263befd21..4d033bc99 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) =
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCalias kn' -> get_alias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
        | _ -> p
 
 (*i Global environment *)
-- 
cgit v1.2.3