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.

2 files changed, 9 insertions, 5 deletions

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 *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2e71b98062..a3441aa3ec 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -248,10 +248,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
   let tps = 
-    match proj with
-    | None -> Cemitcodes.from_val (compile_constant_body env def)
-    | Some pb ->
-      Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
+    (* FIXME: incompleteness of the bytecode vm: we compile polymorphic 
+       constants like opaque definitions. *)
+    if poly then Cemitcodes.from_val Cemitcodes.BCconstant
+    else
+      match proj with
+      | None -> Cemitcodes.from_val (compile_constant_body env def)
+      | Some pb ->
+	Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
   in
   { const_hyps = hyps;
     const_body = def;