diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 0f6e09521..a1b0c697c 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -166,7 +166,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; |