Actually deprecate the `cutrewrite` tactic

The manual was already saying that it was deprecated, but no warning was
emitted.

Fixes #10572

5 files changed, 18 insertions, 11 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 2c245e7d9b..81e50c0834 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2824,11 +2824,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    .. tacv:: cutrewrite <- (@term = @term’)
       :name: cutrewrite
 
-      This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`.
+      .. deprecated:: 8.5
+
+         This tactic can be replaced by :n:`enough (@term = @term’) as <-`.
 
    .. tacv:: cutrewrite -> (@term = @term’)
 
-      This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`.
+      .. deprecated:: 8.5
+
+         This tactic can be replaced by :n:`enough (@term = @term’) as ->`.
 
 
 .. tacn:: subst @ident
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index b90e44eed8..4a603f2c52 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -472,8 +472,8 @@ intros k i p H; induction H; simpl poly_mul_mon; case_decide; intuition.
   - match goal with [ H : null ?p |- _ ] => solve[inversion H] end.
 + apply (valid_le_compat k); auto; constructor; intuition.
   - assert (X := poly_mul_mon_null_compat); intuition eauto.
-  - cutrewrite <- (Pos.max (Pos.succ i) i0 = i0); intuition.
-  - cutrewrite <- (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0); intuition.
+  - enough (Pos.max (Pos.succ i) i0 = i0) as <-; intuition.
+  - enough (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0) as <-; intuition.
 Qed.
 
 Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index a9e5271e81..6c63a891e8 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -203,10 +203,6 @@ TACTIC EXTEND dependent_rewrite
     -> { rewriteInHyp b c id }
 END
 
-(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
-    "replace u with t" or "enough (t=u) as <-" and
-    "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
-
 TACTIC EXTEND cut_rewrite
 | [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
 | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fc37d5a254..96b61b6994 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1648,7 +1648,14 @@ let cutSubstClause l2r eqn cls =
     | None ->    cutSubstInConcl l2r eqn
     | Some id -> cutSubstInHyp l2r eqn id
 
-let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls)
+let warn_deprecated_cutrewrite =
+  CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
+    (fun () -> strbrk"\"cutrewrite\" is deprecated. See documentation for proposed replacement.")
+
+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
 
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index be33104918..4c0ee1b5bd 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -35,8 +35,8 @@ Module Pair (X: PO) (Y: PO) <: PO.
     destruct p2.
     unfold le.
      intuition.
-     cutrewrite (t = t1).
-     cutrewrite (t0 = t2).
+     enough (t = t1) as ->.
+     enough (t0 = t2) as ->.
     reflexivity.
 
     info auto.