Merge PR #6713: Fix #6677: Critical bug with VM and universes

1 files changed, 6 insertions, 5 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 1102cdec18..2d8a1d9761 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,6 +8,7 @@
 open Names
 open Sorts
 open Cbytecodes
+open Univ
 
 (*******************************************)
 (* Initalization of the abstract machine ***)
@@ -189,11 +190,11 @@ let rec whd_accu a stk =
   | i when Int.equal i type_atom_tag ->
      begin match stk with
      | [Zapp args] ->
-        let u = ref (Obj.obj (Obj.field at 0)) in
-        for i = 0 to nargs args - 1 do
-          u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
-        done;
-        Vsort (Type !u)
+        let args = Array.init (nargs args) (arg args) in
+        let u = Obj.obj (Obj.field at 0) in
+        let inst = Instance.of_array (Array.map uni_lvl_val args) in
+        let u = Univ.subst_instance_universe inst u in
+        Vsort (Type u)
      | _ -> assert false
      end
   | i when i <= max_atom_tag ->