From e60721cf3108c569e743e4bc74032ddf35b291dc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 16 Aug 2020 19:26:18 +0200
Subject: 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.)
---
 doc/sphinx/proof-engine/tactics.rst | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3