Merge PR #10575: Clean up deprecations

Reviewed-by: Zimmi48
Reviewed-by: silene

9 files changed, 32 insertions, 12 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4f903d5776..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
@@ -4895,6 +4899,8 @@ Performance-oriented tactic variants
    .. tacv:: convert_concl_no_check @term
       :name: convert_concl_no_check
 
+      .. deprecated:: 8.11
+
       Deprecated old name for :tacn:`change_no_check`. Does not support any of its
       variants.
 
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.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 8d6724c3b1..5f088379ca 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1003,7 +1003,7 @@ GRAMMAR EXTEND Gram
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
           { fun g -> VernacSearch (SearchRewrite c,g, l) }
       | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
-          { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) }
+          { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) }
       (* compatibility: SearchAbout *)
       | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." ->
           { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 080629ede2..1aa9a4e0f5 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -161,6 +161,8 @@ open Pputils
       | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
       | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
       | SearchAbout sl ->
+         keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+      | Search sl ->
          keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
   let pr_option_ref_value = function
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 535aceed15..bb55cd5114 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1785,6 +1785,10 @@ let () =
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
 
+let warn_deprecated_search_about =
+  CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated"
+         (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.")
+
 let vernac_search ~pstate ~atts s gopt r =
   let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
@@ -1815,6 +1819,10 @@ let vernac_search ~pstate ~atts s gopt r =
   | SearchHead c ->
       (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchAbout sl ->
+      warn_deprecated_search_about ();
+      (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+       Search.prioritize_search) pr_search
+  | Search sl ->
       (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
        Search.prioritize_search) pr_search
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ce96d9265c..bec6a0d2bb 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -70,6 +70,7 @@ type searchable =
   | SearchRewrite of constr_pattern_expr
   | SearchHead of constr_pattern_expr
   | SearchAbout of (bool * search_about_item) list
+  | Search of (bool * search_about_item) list
 
 type locatable =
   | LocateAny of qualid or_by_notation