Remove SearchAbout command, deprecated in 8.5

20 files changed, 54 insertions, 121 deletions

diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
new file mode 100644
index 0000000000..e409c638bb
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
@@ -0,0 +1,3 @@
+- **Removed:** Removed SearchAbout command that was deprecated in 8.5.
+  Use :cmd:`Search` instead.
+  (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index c33d62532e..c6a3697916 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -321,18 +321,6 @@ Requests to the environment
 
             Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 
-   .. cmdv:: SearchAbout
-      :name: SearchAbout
-
-      .. deprecated:: 8.5
-
-      Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current
-      :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with
-      command :cmd:`SearchAbout`. For compatibility, the deprecated name
-      :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For
-      compatibility, the list of objects to search when using :cmd:`SearchAbout`
-      may also be enclosed by optional ``[ ]`` delimiters.
-
 
 .. cmd:: SearchHead @term
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 88a5217652..60b845c4be 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1125,10 +1125,6 @@ query_command: [
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
 | REPLACE "Search" searchabout_query searchabout_queries "."
 | WITH "Search" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" searchabout_query searchabout_queries "."
-| WITH "SearchAbout" searchabout_query searchabout_queries
-| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
-| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules
 ]
 
 vernac_toplevel: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 241cf48cf1..272d17bb35 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1244,8 +1244,6 @@ query_command: [
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
 | "Search" searchabout_query searchabout_queries "."
-| "SearchAbout" searchabout_query searchabout_queries "."
-| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "."
 ]
 
 printable: [
@@ -2454,8 +2452,6 @@ as_or_and_ipat: [
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 38e7b781df..0c9d7a853b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -918,8 +918,6 @@ command: [
 | "SearchPattern" one_term OPT ne_in_or_out_modules
 | "SearchRewrite" one_term OPT ne_in_or_out_modules
 | "Search" searchabout_query OPT searchabout_queries
-| "SearchAbout" searchabout_query OPT searchabout_queries
-| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules
 | "Time" command
 | "Redirect" string command
 | "Timeout" num command
@@ -1441,8 +1439,6 @@ as_or_and_ipat: [
 
 eqn_ipat: [
 | "eqn" ":" naming_intropattern
-| "_eqn" ":" naming_intropattern
-| "_eqn"
 ]
 
 as_name: [
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index c5883cef0d..711986c2b2 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -207,7 +207,6 @@ let state_preserving = [
   "Recursive Extraction Library";
 
   "Search";
-  "SearchAbout (* deprecated *)";
   "SearchHead";
   "SearchPattern";
   "SearchRewrite";
diff --git a/ide/microPG.ml b/ide/microPG.ml
index 46d3316ef6..5a4871b70a 100644
--- a/ide/microPG.ml
+++ b/ide/microPG.ml
@@ -289,7 +289,6 @@ let pg = insert pg "Proof General" [mC,_c,"c"; mC,_a,"a"] [
   mkE _p "p" "Print" (Callback (fun gui -> command gui "Print"));
   mkE _c "c" "Check" (Callback (fun gui -> command gui "Check"));
   mkE _b "b" "About" (Callback (fun gui -> command gui "About"));
-  mkE _a "a" "Search About" (Callback (fun gui -> command gui "SearchAbout"));
   mkE _o "o" "Search Pattern" (Callback (fun gui->command gui "SearchPattern"));
   mkE _l "l" "Locate" (Callback (fun gui -> command gui "Locate"));
   mkE _Return "RET" "match template" (Action("Templates","match"));
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index df6189f212..4b78e64d98 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with
 | [] -> accu
 | (flag, arg) :: rem ->
   fun gr env typ ->
-    let ans = Search.search_about_filter arg gr env typ in
+    let ans = Search.search_filter arg gr env typ in
     (if flag then ans else not ans) && interp_search_about rem accu gr env typ
 
 let interp_search_arg arg =
diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v
index 42b1244fb5..caa7373f5e 100644
--- a/test-suite/bugs/closed/HoTT_coq_010.v
+++ b/test-suite/bugs/closed/HoTT_coq_010.v
@@ -1,3 +1,3 @@
-SearchAbout and.
+Search and.
 (* Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v
index 6be2161c2f..ddede74acc 100644
--- a/test-suite/bugs/closed/bug_3900.v
+++ b/test-suite/bugs/closed/bug_3900.v
@@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
 Class Foo (x : Type) := { _ : forall y, y }.
 Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
 Proof.
-SearchAbout ((forall _ _, _) -> Foo _).
+Search ((forall _ _, _) -> Foo _).
 Abort.
diff --git a/test-suite/success/search.v b/test-suite/success/search.v
new file mode 100644
index 0000000000..92de43e052
--- /dev/null
+++ b/test-suite/success/search.v
@@ -0,0 +1,35 @@
+
+(** Test of the different syntaxes of Search *)
+
+Search plus.
+Search plus mult.
+Search "plus_n".
+Search plus "plus_n".
+Search "*".
+Search "*" "+".
+
+Search plus inside Peano.
+Search plus mult inside Peano.
+Search "plus_n" inside Peano.
+Search plus "plus_n" inside Peano.
+Search "*" inside Peano.
+Search "*" "+" inside Peano.
+
+Search plus outside Peano Logic.
+Search plus mult outside Peano Logic.
+Search "plus_n" outside Peano Logic.
+Search plus "plus_n" outside Peano Logic.
+Search "*" outside Peano Logic.
+Search "*" "+" outside Peano Logic.
+
+Search -"*" "+" outside Logic.
+Search -"*"%nat "+"%nat outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+Search Z.mul Z.add "distr".
+Search "+"%Z "*"%Z "distr" -positive -Prop.
+Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
deleted file mode 100644
index 9edfd82556..0000000000
--- a/test-suite/success/searchabout.v
+++ /dev/null
@@ -1,60 +0,0 @@
-
-(** Test of the different syntaxes of SearchAbout, in particular
-    with and without the [ ... ] delimiters *)
-
-SearchAbout plus.
-SearchAbout plus mult.
-SearchAbout "plus_n".
-SearchAbout plus "plus_n".
-SearchAbout "*".
-SearchAbout "*" "+".
-
-SearchAbout plus inside Peano.
-SearchAbout plus mult inside Peano.
-SearchAbout "plus_n" inside Peano.
-SearchAbout plus "plus_n" inside Peano.
-SearchAbout "*" inside Peano.
-SearchAbout "*" "+" inside Peano.
-
-SearchAbout plus outside Peano Logic.
-SearchAbout plus mult outside Peano Logic.
-SearchAbout "plus_n" outside Peano Logic.
-SearchAbout plus "plus_n" outside Peano Logic.
-SearchAbout "*" outside Peano Logic.
-SearchAbout "*" "+" outside Peano Logic.
-
-SearchAbout -"*" "+" outside Logic.
-SearchAbout -"*"%nat "+"%nat outside Logic.
-
-SearchAbout [plus].
-SearchAbout [plus mult].
-SearchAbout ["plus_n"].
-SearchAbout [plus "plus_n"].
-SearchAbout ["*"].
-SearchAbout ["*" "+"].
-
-SearchAbout [plus] inside Peano.
-SearchAbout [plus mult] inside Peano.
-SearchAbout ["plus_n"] inside Peano.
-SearchAbout [plus "plus_n"] inside Peano.
-SearchAbout ["*"] inside Peano.
-SearchAbout ["*" "+"] inside Peano.
-
-SearchAbout [plus] outside Peano Logic.
-SearchAbout [plus mult] outside Peano Logic.
-SearchAbout ["plus_n"] outside Peano Logic.
-SearchAbout [plus "plus_n"] outside Peano Logic.
-SearchAbout ["*"] outside Peano Logic.
-SearchAbout ["*" "+"] outside Peano Logic.
-
-SearchAbout [-"*" "+"] outside Logic.
-SearchAbout [-"*"%nat "+"%nat] outside Logic.
-
-
-(** The example in the Reference Manual *)
-
-Require Import ZArith.
-
-SearchAbout Z.mul Z.add "distr".
-SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
-SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6126d9c37d..71ba3e645d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -43,5 +43,5 @@ Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001).
 (* Printing/Parsing of bytes *)
 Export Byte.ByteSyntaxNotations.
 
-(* Default substrings not considered by queries like SearchAbout *)
+(* Default substrings not considered by queries like Search *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d2b0078a7c..862715753d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -42,7 +42,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
-      "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite";
+      "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dd75693c5b..a8f1a49086 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -983,13 +983,6 @@ GRAMMAR EXTEND Gram
           { fun g -> VernacSearch (SearchRewrite c,g, l) }
       | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
           { 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) }
-      (* compatibility: SearchAbout with "[ ... ]" *)
-      | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]";
-        l = in_or_out_modules; "." ->
-         { fun g -> VernacSearch (SearchAbout sl,g, l) }
       ] ]
   ;
   printable:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a3de88d4dc..054b60853f 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -142,7 +142,7 @@ open Pputils
     | SearchOutside [] -> mt()
     | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
 
-  let pr_search_about (b,c) =
+  let pr_search (b,c) =
     (if b then str "-" else mt()) ++
       match c with
         | SearchSubPattern p ->
@@ -158,10 +158,8 @@ open Pputils
       | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
       | 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
+         keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b
 
   let pr_option_ref_value = function
     | QualidRefValue id -> pr_qualid id
diff --git a/vernac/search.ml b/vernac/search.ml
index ceff8acc79..68a30b4231 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration
 type filter_function = GlobRef.t -> env -> constr -> bool
 type display_function = GlobRef.t -> env -> constr -> unit
 
-(* This option restricts the output of [SearchPattern ...],
-[SearchAbout ...], etc. to the names of the symbols matching the
+(* This option restricts the output of [SearchPattern ...], etc.
+to the names of the symbols matching the
 query, separated by a newline. This type of output is useful for
 editors (like emacs), to generate a list of completion candidates
 without having to parse through the types of all symbols. *)
@@ -226,7 +226,7 @@ let module_filter (mods, outside) ref env typ =
 
 let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
 
-let search_about_filter query gr env typ = match query with
+let search_filter query gr env typ = match query with
 | GlobSearchSubPattern pat ->
   Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ)
 | GlobSearchString s ->
@@ -283,14 +283,14 @@ let search_by_head ?pstate gopt pat mods pr_search =
   in
   generic_search ?pstate gopt iter
 
-(** SearchAbout *)
+(** Search *)
 
-let search_about ?pstate gopt items mods pr_search =
+let search ?pstate gopt items mods pr_search =
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
     module_filter mods ref env typ &&
     List.for_all
-      (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items &&
+      (fun (b,i) -> eqb b (search_filter i ref env typ)) items &&
     blacklist_filter ref env typ
   in
   let iter ref env typ =
diff --git a/vernac/search.mli b/vernac/search.mli
index 11dd0c6794..6dbbff3a8c 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -30,8 +30,7 @@ val blacklist_filter : filter_function
 val module_filter : DirPath.t list * bool -> filter_function
 (** Check whether a reference pertains or not to a set of modules *)
 
-val search_about_filter : glob_search_about_item -> filter_function
-(** Check whether a reference matches a SearchAbout query. *)
+val search_filter : glob_search_about_item -> filter_function
 
 (** {6 Specialized search functions}
 
@@ -45,7 +44,7 @@ val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> D
                   -> display_function -> unit
 val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_about   : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
+val search         : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8641c67d9f..963b5f2084 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1773,10 +1773,6 @@ 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
@@ -1809,12 +1805,8 @@ let vernac_search ~pstate ~atts s gopt r =
       (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
   | 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.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
        Search.prioritize_search) pr_search);
   Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b7c6d3c490..d6e7a3947a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -69,7 +69,6 @@ type searchable =
   | SearchPattern of constr_pattern_expr
   | 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 =