From 46c28054eb404175e5ba9485c3b5efbfe1b81619 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 30 Dec 2020 12:39:53 -0800
Subject: Deprecate "at ... with ..." in change tactic (use "with ... at ..."
 instead)

---
 test-suite/success/change.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3