9 files changed, 6 insertions, 36 deletions
diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
new file mode 100644
index 0000000000..b719c5618e
--- /dev/null
+++ b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
@@ -0,0 +1,4 @@
+- **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/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 72c6ec4ac5..2211a58e6e 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
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 6625e07d05..9971a03894 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1033,9 +1033,6 @@ 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 7f4e92fc37..f628c86cf1 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1535,8 +1535,6 @@ 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 84efc1e36c..3cd5a85654 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1445,7 +1445,6 @@ 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
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 66c72a30a2..4f20e5a800 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin"
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
-(* cutrewrite, dependent rewrite                                      *)
+(* dependent rewrite                                                  *)
 
 let with_delayed_uconstr ist c tac =
   let flags = {
@@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite
     -> { rewriteInHyp b c id }
 END
 
-TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
-| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
-    -> { cutRewriteInHyp b eqn id }
-END
-
 (**********************************************************************)
 (* Decompose                                                          *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 26ae35a79d..8478c1957a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1651,17 +1651,6 @@ let cutSubstClause l2r eqn cls =
     | None ->    cutSubstInConcl l2r eqn
     | Some id -> cutSubstInHyp l2r eqn id
 
-let warn_deprecated_cutrewrite =
-  CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
-    (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.")
-
-let cutRewriteClause l2r eqn cls =
-  warn_deprecated_cutrewrite ();
-  try_rewrite (cutSubstClause l2r eqn cls)
-
-let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
-let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
-
 let substClause l2r c cls =
   Proofview.Goal.enter begin fun gl ->
   let eq = pf_apply get_type_of gl c in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index fdcbbc0e3c..5a4fe47cab 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -107,10 +107,6 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
 
-(* The family cutRewriteIn expect an equality statement *)
-val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic
-val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
-
 (* The family rewriteIn expect the proof of an equality *)
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic