diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 5d82e862b..14aeb732f 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -30,7 +30,6 @@ let popstop_code i = let stop = popstop_code 0 - (************************************************) (* Abstract machine *****************************) (************************************************) @@ -72,7 +71,6 @@ let apply_varray vf varray = interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) @@ -170,7 +168,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; |