From f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 8 Sep 2020 16:51:05 +0200
Subject: Remove deprecated tactic cutrewrite.

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 doc/sphinx/proof-engine/tactics.rst                  | 7 -------
 2 files changed, 1 insertion(+), 8 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7f270e8076..5a11b4f474 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3110,7 +3110,7 @@ An :token:`r_item` can be:
     + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above.
       The tactic: ``rewrite r_prefix (t1 ,…,tn ).``
       is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``
-    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.  tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``.
+    + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above.
 
   .. example::
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index f3dc9a6cb1..cff3f95804 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2819,13 +2819,6 @@ 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
 
-- 
cgit v1.2.3