Deprecate SearchHead.

The main use case of SearchHead is now handled by headconcl:
The secondary use case was redundant with SearchPattern.

2 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 61ceab72f8..9554581ebe 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,9 +1,17 @@
+File "stdin", line 3, characters 0-14:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_n_S: forall n m : nat, n <= m -> S n <= S m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
+File "stdin", line 4, characters 0-16:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 false: bool
 true: bool
 negb: bool -> bool
@@ -27,6 +35,10 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Decimal.int_beq: Decimal.int -> Decimal.int -> bool
 Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
+File "stdin", line 5, characters 0-21:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0
@@ -45,5 +57,13 @@ f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
+File "stdin", line 11, characters 2-20:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 h: newdef n
+File "stdin", line 17, characters 2-15:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 h: P n
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index a860bc8bf6..9de8d6fbc3 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -95,6 +95,12 @@ 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
@@ -123,6 +129,7 @@ let interp_search env sigma s r =
   | 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 |>