diff options
| author | Hugo Herbelin | 2020-12-04 07:46:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-14 19:51:29 +0100 |
| commit | e3968a275532d40009f4ed0e7ea8abbe783e034f (patch) | |
| tree | 72cf1c06159315115633a57ff6bbadecf035fd5a /test-suite | |
| parent | 81d0936c1ac8a537b5d8083933bce607e55ff28f (diff) | |
Add checks for invalid occurrences in setoid rewrite.
We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/rewrite_in.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v index 29fe915ff4..3433866239 100644 --- a/test-suite/success/rewrite_in.v +++ b/test-suite/success/rewrite_in.v @@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True. rewrite H in p || trivial. Qed. - +Goal 1 = 0 -> 0 = 1. + intro H. + Fail rewrite H at 1 2 3. (* bug #13566 *) + Fail rewrite H at 0. + rewrite H at 1. + reflexivity. +Qed. |