diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 988d9f5308..96ddc730e7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -257,8 +257,13 @@ let bind_red_expr_occurrences occs nbcl redexp = error_illegal_clause () else Simpl (Some (occs,c)) + | CbvVm (Some (occl,c)) -> + if occl <> all_occurrences_expr then + error_illegal_clause () + else + CbvVm (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ - | ExtraRedExpr _ | CbvVm | Fold _ | Simpl None -> + | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None -> error_occurrences_not_unsupported () | Unfold [] | Pattern [] -> assert false |