Remove SearchAbout command, deprecated in 8.5

6 files changed, 11 insertions, 30 deletions

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 =