diff options
| author | coqbot-app[bot] | 2021-03-08 20:22:04 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-08 20:22:04 +0000 |
| commit | b55216ab3509f48e45aac035f1b799529d068f51 (patch) | |
| tree | 56deddf678f024309b084951b8f6997d7e303d3d /tactics | |
| parent | 4a0cf0f3fb4a1a57627f22897030771b2921ce85 (diff) | |
| parent | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (diff) | |
Merge PR #13707: Convert 2nd part of rewriting chapter to prodn
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'tactics')
| -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 |