diff options
| author | Pierre-Marie Pédrot | 2021-01-07 18:13:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-07 18:13:28 +0100 |
| commit | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (patch) | |
| tree | 86dd8f3ebcebda8edb2d4ae46793a310e16d062f /test-suite | |
| parent | 331592e05f6f222da40489a94abdcdd3ef4b6394 (diff) | |
| parent | 46c28054eb404175e5ba9485c3b5efbfe1b81619 (diff) | |
Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... at ..." instead)
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/change.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 2f676cf9ad..053429a5a9 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -14,8 +14,8 @@ Abort. (* Check the combination of at, with and in (see bug #2146) *) Goal 3=3 -> 3=3. intro H. -change 3 at 2 with (1+2). -change 3 at 2 with (1+2) in H |-. +change 3 with (1+2) at 2. +change 3 with (1+2) in H at 2 |-. change 3 with (1+2) in H at 1 |- * at 1. (* Now check that there are no more 3's *) change 3 with (1+2) in * || reflexivity. |