From 058ac643c5e93da2472e3a0a717b864f49f90b3b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 27 Nov 2020 16:22:33 +0100
Subject: Revert "Remove deprecated tactic cutrewrite."

This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
---
 doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/sphinx')

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