From d3c3b67c10774ab09054b94c6db5633f0483a06f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 17 Jan 2015 14:11:13 +0530
Subject: Univs: Fix alias computation for VMs, computation of normal form of
 match predicates for vm_compute and compile polymorphic definitions to
 constant code. Add univscompute test-suite file testing VM computations in
 presence of polymorphic universes.

---
 kernel/cbytegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cbytegen.ml')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 65ee655dab..d6c160c3dd 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -490,7 +490,7 @@ let rec get_allias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     (match Cemitcodes.force tps with
-    | BCallias kn' -> get_allias env kn'
+    | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
     | _ -> p)
 
 (* Compiling expressions *)
-- 
cgit v1.2.3