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

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

2 files changed, 3 insertions, 28 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 72970f46b0..665bae7077 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.