Deprecate "at ... with ..." in change tactic

(use "with ... at ..." instead)

6 files changed, 21 insertions, 5 deletions

diff --git a/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst
new file mode 100644
index 0000000000..306fe8052d
--- /dev/null
+++ b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst
@@ -0,0 +1,7 @@
+- **Deprecated:**
+  In :tacn:`change` and :tacn:`change_no_check`, the
+  `at ... with ...` form is deprecated.  Use
+  `with ... at ...` instead.  For `at ... with ... in H |-`,
+  use `with ... in H at ... |-`.
+  (`#13696 <https://github.com/coq/coq/pull/13696>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 07b7928847..8873d02888 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -280,6 +280,9 @@ Rewriting with definitional equality
      whose value which will substituted for `x` in :n:`@one_term__to`, such as in
      `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`.
 
+     The `at ... with ...` form is deprecated in 8.14; use `with ... at ...` instead.
+     For `at ... with ... in H |-`, use `with ... in H at ... |-`.
+
    :n:`@occurrences`
      If `with` is not specified, :n:`@occurrences` must only specify
      entire hypotheses and/or the goal; it must not include any
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 43957bbde5..cb430efb40 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -182,6 +182,11 @@ let merge_occurrences loc cl = function
     in
     (Some p, ans)
 
+let deprecated_conversion_at_with =
+  CWarnings.create
+    ~name:"conversion_at_with" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead.")
+
 (* Auxiliary grammar rules *)
 
 open Pvernac.Vernac_
@@ -230,7 +235,8 @@ GRAMMAR EXTEND Gram
     [ [ c = constr -> { (None, c) }
       | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
       | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
-          { (Some (occs,c1), c2) } ] ]
+          { deprecated_conversion_at_with ();  (* 8.14 *)
+          (Some (occs,c1), c2) } ] ]
   ;
   occs_nums:
     [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
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.
diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v
index 5611329b12..f86246d3c2 100644
--- a/theories/Numbers/DecimalPos.v
+++ b/theories/Numbers/DecimalPos.v
@@ -216,7 +216,7 @@ Proof.
   - trivial.
   - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
     rewrite N.mul_succ_r.
-    change 10 at 2 with (Nat.iter 10%nat N.succ 0).
+    change 10 with (Nat.iter 10%nat N.succ 0) at 2.
     rewrite ?nat_iter_S, nat_iter_0.
     rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
     destruct (to_lu (N.pos p)); simpl; auto.
diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v
index 47f6d983b7..29029cb839 100644
--- a/theories/Numbers/HexadecimalPos.v
+++ b/theories/Numbers/HexadecimalPos.v
@@ -235,7 +235,7 @@ Proof.
   - trivial.
   - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
     rewrite N.mul_succ_r.
-    change 0x10 at 2 with (Nat.iter 0x10%nat N.succ 0).
+    change 0x10 with (Nat.iter 0x10%nat N.succ 0) at 2.
     rewrite ?nat_iter_S, nat_iter_0.
     rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
     destruct (to_lu (N.pos p)); simpl; auto.