diff options
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 1102cdec1..2d8a1d976 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 -> |