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 0f0e43021d..c769fb3ba2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -262,8 +262,13 @@ let bind_red_expr_occurrences occs nbcl redexp = error_illegal_clause () else CbvVm (Some (occs,c)) + | CbvNative (Some (occl,c)) -> + if occl != AllOccurrences then + error_illegal_clause () + else + CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ - | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None -> + | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None | CbvNative None -> error_occurrences_not_unsupported () | Unfold [] | Pattern [] -> assert false |