From 5e849322fe9448f2f79e00194dbe3f196ae31f8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 6 Sep 2023 13:40:04 +0200
Subject: [PATCH] Stop using `assumption` in `replace by tac`

Close #17959
---
 .../17964-SkySkimmer-replace-assum.sh         |  1 +
 .../04-tactics/17964-replace-assum.rst        |  8 ++++++++
 doc/sphinx/proofs/writing-proofs/equality.rst |  4 ++--
 tactics/equality.ml                           | 19 +++++++++----------
 4 files changed, 20 insertions(+), 12 deletions(-)
 create mode 100644 dev/ci/user-overlays/17964-SkySkimmer-replace-assum.sh
 create mode 100644 doc/changelog/04-tactics/17964-replace-assum.rst

diff --git a/dev/ci/user-overlays/17964-SkySkimmer-replace-assum.sh b/dev/ci/user-overlays/17964-SkySkimmer-replace-assum.sh
new file mode 100644
index 0000000000000..8ba032c354fba
--- /dev/null
+++ b/dev/ci/user-overlays/17964-SkySkimmer-replace-assum.sh
@@ -0,0 +1 @@
+overlay bedrock2 https://github.com/SkySkimmer/bedrock2 replace-assum 17964
diff --git a/doc/changelog/04-tactics/17964-replace-assum.rst b/doc/changelog/04-tactics/17964-replace-assum.rst
new file mode 100644
index 0000000000000..565a74e2381ce
--- /dev/null
+++ b/doc/changelog/04-tactics/17964-replace-assum.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+  :tacn:`replace` with `by tac` does not automatically attempt to solve
+  the generated equality subgoal using the hypotheses.
+  Use `by first [assumption | symmetry;assumption | tac]`
+  if you need the previous behaviour
+  (`#17964 <https://github.com/coq/coq/pull/17964>`_,
+  fixes `#17959 <https://github.com/coq/coq/issues/17959>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst
index ee57c0ebb06d0..8310e4ddbdc5d 100644
--- a/doc/sphinx/proofs/writing-proofs/equality.rst
+++ b/doc/sphinx/proofs/writing-proofs/equality.rst
@@ -248,8 +248,8 @@ Rewriting with Leibniz and setoid equality
    as a subgoal. (Note the generated equality is reversed with respect
    to the order of the two terms in the tactic syntax; see
    issue `#13480 <https://github.com/coq/coq/issues/13480>`_.)
-   This equality is automatically solved if it occurs among
-   the hypotheses, or if its symmetric form occurs.
+   When :n:`by @ltac_expr3` is not present, this equality is automatically solved
+   if it occurs among the hypotheses, or if its symmetric form occurs.
 
    The second form, with `->` or no arrow, replaces :n:`@one_term__from`
    with :n:`@term__to` using
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 202b40a2353f3..a1055d0563fb9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -620,11 +620,6 @@ let replace_core clause l2r eq =
    gl : goal *)
 
 let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
-  let try_prove_eq =
-    match try_prove_eq_opt with
-      | None -> Proofview.tclUNIT ()
-      | Some tac ->  tclCOMPLETE tac
-  in
   Proofview.Goal.enter begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
   let t1 = get_type_of c1
@@ -648,13 +643,17 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     Tacticals.pf_constr_of_global sym >>= fun sym ->
     Tacticals.pf_constr_of_global e >>= fun e ->
     let eq = applist (e, [t1;c1;c2]) in
+    let solve_tac = match try_prove_eq_opt with
+      | None ->
+        tclFIRST
+          [ assumption;
+            tclTHEN (apply sym) assumption;
+            Proofview.tclUNIT () ]
+      | Some tac -> tclCOMPLETE tac
+    in
     tclTHENLAST
       (replace_core clause l2r eq)
-      (tclFIRST
-         [assumption;
-          tclTHEN (apply sym) assumption;
-          try_prove_eq
-         ])
+      solve_tac
   end
 
 let replace c1 c2 =