diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2021-03-08 11:48:20 -0800 |
| commit | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (patch) | |
| tree | 864068cd317abebcbc0a3466a1365258729fbc40 /tactics/redexpr.ml | |
| parent | fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a (diff) | |
Convert 2nd part of rewriting chapter to prodn
Diffstat (limited to 'tactics/redexpr.ml')
| -rw-r--r-- | tactics/redexpr.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 87cae3abe5..3ee85f6b1b 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -271,11 +271,14 @@ let reduction_of_red_expr env r = let error_illegal_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.") +let error_multiple_patterns () = + CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.") + let error_illegal_non_atomic_clause () = CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.") -let error_occurrences_not_unsupported () = - CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.") +let error_at_in_occurrences_not_supported () = + CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.") let bind_red_expr_occurrences occs nbcl redexp = let open Locus in @@ -292,14 +295,14 @@ let bind_red_expr_occurrences occs nbcl redexp = else match redexp with | Unfold (_::_::_) -> - error_illegal_clause () + error_multiple_patterns () | Unfold [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () else Unfold [(occs,c)] | Pattern (_::_::_) -> - error_illegal_clause () + error_multiple_patterns () | Pattern [(occl,c)] -> if occl != AllOccurrences then error_illegal_clause () @@ -322,7 +325,7 @@ let bind_red_expr_occurrences occs nbcl redexp = CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> - error_occurrences_not_unsupported () + error_at_in_occurrences_not_supported () | Unfold [] | Pattern [] -> assert false |