Recommend replace as a replacement to cutrewrite.

As suggested by Laurent Thery to Chris Dams on Coq-Club.

(And fix the documented syntax in the manual.)

1 files changed, 2 insertions, 9 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index c5fab0983f..8635add0e1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2819,19 +2819,12 @@ 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 = @term’)
+   .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident }
       :name: cutrewrite
 
       .. deprecated:: 8.5
 
-         This tactic can be replaced by :n:`enough (@term = @term’) as <-`.
-
-   .. tacv:: cutrewrite -> (@term = @term’)
-
-      .. deprecated:: 8.5
-
-         This tactic can be replaced by :n:`enough (@term = @term’) as ->`.
-
+         Use :tacn:`replace` instead.
 
 .. tacn:: subst @ident
    :name: subst