Stop using assumption in replace by tac

Close #17959

dev/ci/user-overlays/17964-SkySkimmer-replace-assum.sh

@@ -0,0 +1 @@
+overlay bedrock2 https://github.com/SkySkimmer/bedrock2 replace-assum 17964

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).

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

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 =