Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."

Reviewed-by: gares

1 files changed, 7 insertions, 0 deletions

diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 2de6b2a18c..b7f2927000 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -146,6 +146,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       only in the conclusion of the goal. The clause argument must not contain
       any ``type of`` nor ``value of``.
 
+   .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident }
+      :name: cutrewrite
+
+      .. deprecated:: 8.5
+
+         Use :tacn:`replace` instead.
+
 .. tacn:: subst @ident
    :name: subst