diff options
| author | Pierre-Marie Pédrot | 2020-12-16 13:39:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-16 13:39:45 +0100 |
| commit | 88c77bf369a910e72951b69b4e272dd50a982bf7 (patch) | |
| tree | bdd8c016188cdc33c40a027d073bc771702335c1 /test-suite | |
| parent | 7c183ac67f8480c64d9f732ce34b6a809c5897b3 (diff) | |
| parent | f3e05c12206c2582c63848fc334c5c758293c707 (diff) | |
Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several tactics.
Reviewed-by: ppedrot
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. |