diff options
| author | Jim Fehrle | 2020-12-30 12:39:53 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-02 22:34:15 -0800 |
| commit | 46c28054eb404175e5ba9485c3b5efbfe1b81619 (patch) | |
| tree | bc333811872b07448b765481b7fab486aeb97323 /test-suite | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Deprecate "at ... with ..." in change tactic
(use "with ... at ..." instead)
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. |