aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst4
-rw-r--r--doc/sphinx/changes.rst2
-rw-r--r--doc/sphinx/proof-engine/tactics.rst2
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst29
-rw-r--r--ide/coqide/coq_commands.ml1
-rw-r--r--test-suite/output/SearchHead.v19
-rw-r--r--test-suite/output/Search_headconcl.out (renamed from test-suite/output/SearchHead.out)20
-rw-r--r--test-suite/output/Search_headconcl.v18
-rw-r--r--tools/coqdoc/output.ml2
-rw-r--r--vernac/comSearch.ml9
-rw-r--r--vernac/g_vernac.mlg2
-rw-r--r--vernac/ppvernac.ml1
-rw-r--r--vernac/search.ml21
-rw-r--r--vernac/search.mli2
-rw-r--r--vernac/vernacexpr.ml1
15 files changed, 27 insertions, 106 deletions
diff --git a/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst
new file mode 100644
index 0000000000..7f0650d8ee
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ SearchHead command. Use the `headconcl:` clause of :cmd:`Search` instead
+ (`#13763 <https://github.com/coq/coq/pull/13763>`_,
+ by Jim Fehrle).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d9e4e4f2b3..b05c6e949c 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1301,7 +1301,7 @@ Commands
Declaration of arbitrary terms as hints. Global references are now
preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by
Pierre-Marie Pédrot).
-- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:`
+- **Deprecated:** `SearchHead` in favor of the new `headconcl:`
clause of :cmd:`Search` (part of `#8855
<https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
- **Added:**
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 766f7ab44e..888a18a3ad 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -77,7 +77,7 @@ specified, the default selector is used.
.. todo: fully describe selectors. At the moment, ltac has a fairly complete description
.. todo: mention selectors can be applied to some commands, such as
- Check, Search, SearchHead, SearchPattern, SearchRewrite.
+ Check, Search, SearchPattern, SearchRewrite.
.. opt:: Default Goal Selector "@toplevel_selector"
:name: Default Goal Selector
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8e2f577f6b..8d1817b61f 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -312,31 +312,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
Search is:Instance [ Reflexive | Symmetric ].
-.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } }
-
- .. deprecated:: 8.12
-
- Use the `headconcl:` clause of :cmd:`Search` instead.
-
- Displays the name and type of all hypotheses of the
- selected goal (if any) and theorems of the current context that have the
- form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern`
- matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b`
- matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`.
-
- See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
-
- .. example:: :cmd:`SearchHead` examples
-
- .. coqtop:: none reset
-
- Add Search Blacklist "internal_".
-
- .. coqtop:: all warn
-
- SearchHead le.
- SearchHead (@eq bool).
-
.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } }
Displays the name and type of all hypotheses of the
@@ -384,7 +359,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
.. table:: Search Blacklist @string
Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
- :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose
+ :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose
fully-qualified name contains any of the strings will be excluded from the
search results. The default blacklisted substrings are ``_subterm``, ``_subproof`` and
``Private_``.
@@ -395,7 +370,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
.. flag:: Search Output Name Only
This flag restricts the output of search commands to identifier names;
- turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`,
+ turning it on causes invocations of :cmd:`Search`,
:cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
output, printing only identifiers.
diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 711986c2b2..2d75ad9ff6 100644
--- a/ide/coqide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
@@ -207,7 +207,6 @@ let state_preserving = [
"Recursive Extraction Library";
"Search";
- "SearchHead";
"SearchPattern";
"SearchRewrite";
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.
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 50aa658128..9cb3baf92c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -42,7 +42,7 @@ let is_keyword =
"Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
- "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite";
+ "Search"; "SearchPattern"; "SearchRewrite";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
"Delimit"; "Bind"; "Open"; "Scope"; "Inline";
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:31:53 +0000