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

Reviewed-by: gares

5 files changed, 13 insertions, 4 deletions

diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
deleted file mode 100644
index b719c5618e..0000000000
--- a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  Deprecated ``cutrewrite`` tactic. Use :tacn:`replace` instead
-  (`#12993 <https://github.com/coq/coq/pull/12993>`_,
-  by Théo Zimmermann).
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
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 8efda825de..75b3260166 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1021,6 +1021,9 @@ simple_tactic: [
 | DELETE "unify" constr constr
 | REPLACE "unify" constr constr "with" preident
 | WITH "unify" constr constr OPT ( "with" preident )
+| DELETE "cutrewrite" orient constr
+| REPLACE "cutrewrite" orient constr "in" hyp
+| WITH "cutrewrite" orient constr OPT ( "in" hyp )
 | DELETE "destauto"
 | REPLACE "destauto" "in" hyp
 | WITH "destauto" OPT ( "in" hyp )
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index cf90eea5a1..ccf38d2c15 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1583,6 +1583,8 @@ simple_tactic: [
 | "simple" "injection" destruction_arg
 | "dependent" "rewrite" orient constr
 | "dependent" "rewrite" orient constr "in" hyp
+| "cutrewrite" orient constr
+| "cutrewrite" orient constr "in" hyp
 | "decompose" "sum" constr
 | "decompose" "record" constr
 | "absurd" constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 7c709baa48..d950b32160 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1685,6 +1685,7 @@ simple_tactic: [
 | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
 | "simple" "injection" OPT destruction_arg
 | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
+| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term