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 --- .../13763-remove_searchhead.rst | 4 +++ doc/sphinx/changes.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 2 +- doc/sphinx/proof-engine/vernacular-commands.rst | 29 ++-------------------- 4 files changed, 8 insertions(+), 29 deletions(-) create mode 100644 doc/changelog/07-vernac-commands-and-options/13763-remove_searchhead.rst (limited to 'doc') 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 `_, + 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 `_, 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 `_, 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. -- cgit v1.2.3