diff options
Diffstat (limited to 'kernel/vmbytegen.ml')
| -rw-r--r-- | kernel/vmbytegen.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 3dc268ccdf..9500b88e60 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont = | None -> if nargs <= 4 then comp_args comp_arg cenv args sz - (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) + (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: @@ -765,7 +765,7 @@ let rec compile_lam env cenv lam sz cont = let (jump, cont) = make_branch cont in let lbl_default = Label.create () in let default = - let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = [Kgetglobal kn; Kshort_apply (arity + Univ.Instance.length u); jump] in let cont = if Univ.Instance.is_empty u then cont else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) |