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.

4 files changed, 43 insertions, 7 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 65ee655da..d6c160c3d 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 2e71b9806..a3441aa3e 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;
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3f1e6e5d6..19613c4e0 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -195,7 +195,7 @@ and nf_stk env c t stk  =
       let pT =
 	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
       let pT = whd_betadeltaiota env pT in
-      let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
+      let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env ind mib mip u params dep p in
       (* calcul des branches *)
@@ -226,7 +226,7 @@ and nf_predicate env ind mip params v pT =
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
       let params = if Int.equal n 0 then params else Array.map (lift n) params in
-      let dom = mkApp(mkInd ind,Array.append params rargs) in
+      let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (name,None,dom) env) vb in
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
diff --git a/test-suite/success/univscompute.v b/test-suite/success/univscompute.v
new file mode 100644
index 000000000..1d60ab360
--- /dev/null
+++ b/test-suite/success/univscompute.v
@@ -0,0 +1,32 @@
+Set Universe Polymorphism.
+
+Polymorphic Definition id {A : Type} (a : A) := a.
+
+Eval vm_compute in id 1.
+
+Polymorphic Inductive ind (A : Type) := cons : A -> ind A.
+
+Eval vm_compute in ind unit.
+
+Check ind unit.
+
+Eval vm_compute in ind unit.
+
+Definition bar := Eval vm_compute in ind unit.
+Definition bar' := Eval vm_compute in id (cons _ tt).
+
+Definition bar'' := Eval native_compute in id 1.
+Definition bar''' := Eval native_compute in id (cons _ tt).
+
+Definition barty := Eval native_compute in id (cons _ Set).
+
+Definition one := @id.
+
+Monomorphic Definition sec := one.
+
+Eval native_compute in sec.
+Definition sec' := Eval native_compute in sec.
+Eval vm_compute in sec.
+Definition sec'' := Eval vm_compute in sec.
+
+