From 3d46bed76e656d6a0e4d87320e4d0fd67d1211c2 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 11:55:49 -0800
Subject: Remove the SearchHead command

---
 vernac/comSearch.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'vernac/comSearch.ml')

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);
-- 
cgit v1.2.3