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.

1 files changed, 8 insertions, 4 deletions

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;