Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

6 files changed, 0 insertions, 36 deletions

diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index af51f4fafb..1b811f3db7 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -105,12 +105,6 @@ let () =
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
 
-let deprecated_searchhead =
-  CWarnings.create
-    ~name:"deprecated-searchhead"
-    ~category:"deprecated"
-    (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead."))
-
 let interp_search env sigma s r =
   let r = interp_search_restriction r in
   let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in
@@ -138,9 +132,6 @@ let interp_search env sigma s r =
       (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | SearchRewrite c ->
       (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
-  | SearchHead c ->
-      deprecated_searchhead ();
-      (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search
   | Search sl ->
       (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
        Search.prioritize_search) pr_search);
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5c329f60a9..f8a28332b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -965,8 +965,6 @@ GRAMMAR EXTEND Gram
       (* Searching the environment *)
       | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
          { fun g -> VernacPrint (PrintAbout (qid,l,g)) }
-      | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
-          { fun g -> VernacSearch (SearchHead c,g, l) }
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
           { fun g -> VernacSearch (SearchPattern c,g, l) }
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index ff4365c8d3..8e5942440b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -242,7 +242,6 @@ let pr_search a gopt b pr_p =
   pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
   ++
   match a with
-  | 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
   | Search sl ->
diff --git a/vernac/search.ml b/vernac/search.ml
index 501e5b1a91..98e231de19 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -185,14 +185,6 @@ let rec pattern_filter pat ref env sigma typ =
   | LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
   | _ -> false
 
-let rec head_filter pat ref env sigma typ =
-  let typ = Termops.strip_outer_cast sigma typ in
-  if Constr_matching.is_matching_head env sigma pat typ then true
-  else match EConstr.kind sigma typ with
-  | Prod (_, _, typ)
-  | LetIn (_, _, _, typ) -> head_filter pat ref env sigma typ
-  | _ -> false
-
 let full_name_of_reference ref =
   let (dir,id) = repr_path (Nametab.path_of_global ref) in
   DirPath.to_string dir ^ "." ^ Id.to_string id
@@ -274,19 +266,6 @@ let search_rewrite env sigma pat mods pr_search =
 
 (** Search *)
 
-let search_by_head env sigma pat mods pr_search =
-  let filter ref kind env typ =
-    module_filter mods ref kind env sigma typ &&
-    head_filter pat ref env sigma (EConstr.of_constr typ) &&
-    blacklist_filter ref kind env sigma typ
-  in
-  let iter ref kind env typ =
-    if filter ref kind env typ then pr_search ref kind env typ
-  in
-  generic_search env iter
-
-(** Search *)
-
 let search env sigma items mods pr_search =
   let filter ref kind env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
diff --git a/vernac/search.mli b/vernac/search.mli
index 09847f4e03..6557aa5986 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -47,8 +47,6 @@ val search_filter : glob_search_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
-                  -> display_function -> unit
 val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
 val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2e360cf969..46acaf7264 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -75,7 +75,6 @@ type search_request =
 type searchable =
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
-  | SearchHead of constr_pattern_expr
   | Search of (bool * search_request) list
 
 type locatable =