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

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

3 files changed, 18 insertions, 39 deletions

diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v
deleted file mode 100644
index 2ee8a0d184..0000000000
--- a/test-suite/output/SearchHead.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Some tests of the Search command *)
-
-SearchHead le.				(* app nodes *)
-SearchHead bool. 				(* no apps *)
-SearchHead (@eq nat).			(* complex pattern *)
-
-Definition newdef := fun x:nat => x = x.
-
-Goal forall n:nat, newdef n -> False.
-  intros n h.
-  SearchHead newdef.             (* search hypothesis *)
-Abort.
-
-
-Goal forall n (P:nat -> Prop), P n -> False.
-  intros n P h.
-  SearchHead P.                  (* search hypothesis also for patterns *)
-Abort.
-
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out
index 2f0d854ac6..24e2ee76af 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/Search_headconcl.out
@@ -1,17 +1,9 @@
-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
@@ -35,10 +27,6 @@ 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
@@ -57,13 +45,5 @@ 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/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v
new file mode 100644
index 0000000000..8b168dcd25
--- /dev/null
+++ b/test-suite/output/Search_headconcl.v
@@ -0,0 +1,18 @@
+(* Some tests of the Search command *)
+
+Search headconcl: le.				(* app nodes *)
+Search headconcl: bool. 				(* no apps *)
+Search headconcl: (@eq nat).			(* complex pattern *)
+
+Definition newdef := fun x:nat => x = x.
+
+Goal forall n:nat, newdef n -> False.
+  intros n h.
+  Search headconcl: newdef.             (* search hypothesis *)
+Abort.
+
+
+Goal forall n (P:nat -> Prop), P n -> False.
+  intros n P h.
+  Search headconcl: P.                  (* search hypothesis also for patterns *)
+Abort.