Document new Search features.

6 files changed, 338 insertions, 70 deletions

diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 34a48b368b..510a97d171 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -6,12 +6,9 @@ Setting properties of a function's arguments
 .. cmd:: Arguments @smart_qualid {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
    :name: Arguments
 
-   .. insertprodn smart_qualid args_modifier
+   .. insertprodn argument_spec args_modifier
 
    .. prodn::
-      smart_qualid ::= @qualid
-      | @by_notation
-      by_notation ::= @string {? % @scope_key }
       argument_spec ::= {? ! } @name {? % @scope_key }
       arg_specs ::= @argument_spec
       | /
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 4be18ccda9..f8435fcffe 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5464,6 +5464,17 @@ equivalences are indeed taken into account, otherwise only single
 .. cmd:: Search {? @pattern }  {* {? - } {| @string | @pattern } {? % @ident} } {? in {+ {? - } @qualid } }
    :name: Search (ssreflect)
 
+   .. versionchanged:: 8.12
+
+      This command is only available when loading a separate plugin
+      (`ssrsearch`).
+
+   .. deprecated:: 8.12
+
+      This command is deprecated since all the additional features it
+      provides have been integrated in the standard :cmd:`Search`
+      command.
+
    This is the |SSR| extension of the Search command. :token:`qualid` is the
    name of an open module. This command returns the list of lemmas:
 
@@ -5502,7 +5513,11 @@ equivalences are indeed taken into account, otherwise only single
         Unset Strict Implicit.
         Unset Printing Implicit Defensive.
 
-     .. coqtop:: all
+     .. coqtop:: in
+
+        Require Import ssrsearch.
+
+     .. coqtop:: all warn
 
         Search "~~".
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7191444bac..1aa363fed5 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -96,38 +96,125 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
 
    .. seealso:: Section :ref:`performingcomputations`.
 
-.. cmd:: Search {+ {? - } @search_item } {? {| inside | outside } {+ @qualid } }
+.. cmd:: Search {+ @search_query } {? {| inside | outside } {+ @qualid } }
 
-   .. insertprodn search_item search_item
+   This command can be used to filter the goal and the global context
+   to retrieve objects whose name or type satisfies a number of
+   conditions.  Library files that were not loaded with :cmd:`Require`
+   are not considered.  The :table:`Search Blacklist` table can also
+   be used to exclude some things from all calls to :cmd:`Search`.
+
+   The output of the command is a list of qualified identifiers and
+   their types.  If the :flag:`Search Output Name Only` flag is on,
+   the types are omitted.
+
+   .. insertprodn search_query search_query
 
    .. prodn::
-      search_item ::= @one_term
-      | @string {? % @scope_key }
+      search_query ::= @search_item
+      | - @search_query
+      | [ {+| {+ @search_query } } ]
 
-   Displays the name and type of all hypotheses of the
-   selected goal (if any) and theorems of the current context
-   matching :n:`@search_item`\s.
-   It's useful for finding the names of library lemmas.
+   Multiple :n:`@search_item`\s can be combined into a complex
+   :n:`@search_query`:
 
-   * :n:`@one_term` - Search for objects containing a subterm matching the pattern
-     :n:`@one_term` in which holes of the pattern are indicated by `_` or :n:`?@ident`.
-     If the same :n:`?@ident` occurs more than once in the pattern, all occurrences must
-     match the same value.
+   :n:`- @search_query`
+      Excludes the objects that would be filtered by
+      :n:`@search_query`.  Cf. :ref:`this example
+      <search-disambiguate-notation>`.
 
-   * :n:`@string` - If :n:`@string` is a substring of a valid identifier,
-     search for objects whose name contains :n:`@string`. If :n:`@string` is a notation
-     string associated with a :n:`@qualid`, that's equivalent to :cmd:`Search` :n:`@qualid`.
-     For example, specifying `"+"` or `"_ + _"`, which are notations for `Nat.add`, are equivalent
-     to :cmd:`Search` `Nat.add`.
+   :n:`[ @search_query ... @search_query | ... | @search_query ... @search_query ]`
+      This is a disjunction of conjunctions of queries.  A simple
+      conjunction can be expressed by having a single disjunctive
+      branch.  For a conjunction at top-level, the surrounding
+      brackets are not required.
 
-   * :n:`% @scope` - limits the search to the scope bound to
-     the delimiting key :n:`@scope`, such as, for example, :n:`%nat`.
-     This clause may be used only if :n:`@string` contains a notation string.
-     (see Section :ref:`LocalInterpretationRulesForNotations`)
+   .. insertprodn search_item search_item
 
-   If you specify multiple :n:`@search_item`\s, all the conditions must be satisfied
-   for the object to be displayed.  The minus sign `-` excludes objects that contain
-   the :n:`@search_item`.
+   .. prodn::
+      search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key }
+      | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term
+      | is : @logical_kind
+
+   Searched objects can be filtered by patterns, by the constants they
+   contain (identified by their name or a notation) and by their
+   names.
+   The location of the pattern or constant within a term
+
+   :n:`@one_term`
+      Search for objects whose type contains a subterm matching the
+      pattern :n:`@one_term`.  Holes of the pattern are indicated by
+      `_` or :n:`?@ident`.  If the same :n:`?@ident` occurs more than
+      once in the pattern, all occurrences in the subterm must be
+      identical.  Cf. :ref:`this example <search-pattern>`.
+
+   :n:`@string {? % @scope_key }`
+      - If :n:`@string` is a substring of a valid identifier and no
+        :n:`% @scope_key` is provided, search for objects whose name
+        contains :n:`@string`.  Cf. :ref:`this example
+        <search-part-ident>`.
+
+      - If :n:`@string` is not a substring of a valid identifier or if
+        the optional :n:`% @scope_key` is provided, search for objects
+        whose type contains the reference that this string,
+        interpreted as a notation, is attached to (as in
+        :n:`@smart_qualid`).  Cf. :ref:`this example
+        <search-by-notation>`.
+
+      .. note::
+
+         If the string is a substring of a valid identifier but you
+         still want to look for a reference by notation, you can put
+         it between single quotes or provide a scope explictly.
+         Cf. :ref:`this example <search-disambiguate-notation>`.
+
+   :n:`hyp:`
+      The provided pattern or reference is matched against any subterm
+      of an hypothesis of the type of the objects.  Cf. :ref:`this
+      example <search-hyp>`.
+
+   :n:`headhyp:`
+      The provided pattern or reference is matched against the
+      subterms in head position (any partial applicative subterm) of
+      the hypotheses of the type of the objects.  Cf. :ref:`the
+      previous example <search-hyp>`.
+
+   :n:`concl:`
+      The provided pattern or reference is matched against any subterm
+      of the conclusion of the type of the objects.  Cf. :ref:`this
+      example <search-concl>`.
+
+   :n:`headconcl:`
+      The provided pattern or reference is matched against the
+      subterms in head position (any partial applicative subterm) of
+      the conclusion of the type of the objects.  Cf. :ref:`the
+      previous example <search-concl>`.
+
+   :n:`head:`
+      This is simply the union between `headconcl:` and `headhyp:`.
+
+   :n:`is: @logical_kind`
+      .. insertprodn logical_kind logical_kind
+
+      .. prodn::
+         logical_kind ::= @thm_token
+         | @assumption_token
+         | Context
+         | Definition
+         | Example
+         | Coercion
+         | Instance
+         | Scheme
+         | Canonical
+         | Field
+         | Method
+         | Primitive
+
+      Filters objects by the keyword that was used to define them
+      (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`,
+      `Primitive`...) or its status (`Coercion`, `Instance`, `Scheme`,
+      `Canonical`, `Field` for record fields, `Method` for class
+      fields).  Cf. :ref:`this example <search-by-keyword>`.
 
    Additional clauses:
 
@@ -139,32 +226,123 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
       There is no constant in the environment named :n:`@qualid`, where :n:`@qualid`
       is in an `inside` or `outside` clause.
 
-   .. example:: :cmd:`Search` examples
+   .. _search-pattern:
 
-      .. coqtop:: in
+   .. example:: Searching for a pattern
+
+      .. coqtop:: none reset
+
+         Require Import PeanoNat.
+
+      We can repeat meta-variables to narrow down the search.  Here,
+      we are looking for commutativity lemmas.
+
+      .. coqtop:: all
+
+         Search (_ ?n ?m = _ ?m ?n).
+
+   .. _search-part-ident:
+
+   .. example:: Searching for part of an identifier
+
+      .. coqtop:: all reset
+
+         Search "_assoc".
+
+   .. _search-by-notation:
+
+   .. example:: Searching for a reference by notation
+
+      .. coqtop:: all reset
+
+         Search "+".
+
+   .. _search-disambiguate-notation:
+
+   .. example:: Disambiguating between part of identifier and notation
+
+      .. coqtop:: none reset
+
+         Require Import PeanoNat.
+
+      In this example, we show two ways of searching for all the
+      objects whose type contains `Nat.modulo` but which do not
+      contain the substring "mod".
+
+      .. coqtop:: all
+
+         Search "'mod'" -"mod".
+         Search "mod"%nat -"mod".
+
+   .. _search-hyp:
+
+   .. example:: Search in hypotheses
+
+      The following search shows the objects whose type contains
+      `bool` in an hypothesis as a strict subterm only:
+
+      .. coqtop:: none reset
+
+         Add Search Blacklist "internal_".
 
-         Require Import ZArith.
+      .. coqtop:: all
+
+         Search hyp:bool -headhyp:bool.
+
+   .. _search-concl:
+
+   .. example:: Search in conclusion
+
+      The following search shows the objects whose type contains `bool`
+      in the conclusion as a strict subterm only:
 
       .. coqtop:: all
 
-         Search Z.mul Z.add "distr".
-         Search "+"%Z "*"%Z "distr" -Prop.
-         Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
+         Search concl:bool -headconcl:bool.
+
+   .. _search-by-keyword:
+
+   .. example:: Search by keyword or status
+
+      The following search shows the definitions whose type is a `nat`
+      or a function which returns a `nat` and the lemmas about `+`:
+
+      .. coqtop:: all reset
 
+         Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
+
+      The following search shows the instances whose type includes the
+      classes `Reflexive` or `Symmetric`:
+
+      .. coqtop:: none reset
+
+         Require Import Morphisms.
+
+      .. coqtop:: all
+
+         Search is:Instance [ Reflexive | Symmetric ].
 
 .. cmd:: SearchHead @one_term {? {| 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_term`
-   matches a prefix of `C`.  For example, a :n:`@one_term` of `f _ b`
-   matches `f a b`, which is a prefix of `C` when `C` is `f a b c`.
+   matches a subterm of `C` in head position.  For example, a :n:`@one_term` 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:: reset all
+      .. coqtop:: none reset
+
+         Add Search Blacklist "internal_".
+
+      .. coqtop:: all warn
 
          SearchHead le.
          SearchHead (@eq bool).
@@ -225,6 +403,12 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
    Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of
    blacklisted strings.
 
+.. 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`,
+   :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
+   output, printing only identifiers.
 
 .. _requests-to-the-environment:
 
@@ -253,6 +437,13 @@ Requests to the environment
 
 .. cmd:: Locate @smart_qualid
 
+   .. insertprodn smart_qualid by_notation
+
+   .. prodn::
+      smart_qualid ::= @qualid
+      | @by_notation
+      by_notation ::= @string {? % @scope_key }
+
    Displays the full name of objects from |Coq|'s various qualified namespaces such as terms,
    modules and Ltac.  It also displays notation definitions.
 
@@ -706,13 +897,6 @@ Controlling display
    interpreted from left to right, so in case of an overlap, the flags on the
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
-.. 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`,
-   :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
-   output, printing only identifiers.
-
 .. opt:: Printing Width @num
    :name: Printing Width
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4149ea7a76..a9a243868f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -60,6 +60,7 @@ DELETE: [
 | test_only_starredidentrefs
 | test_bracket_ident
 | test_hash_ident
+| test_id_colon
 | test_lpar_id_colon
 | test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
@@ -1232,8 +1233,8 @@ query_command: [
 | WITH "SearchPattern" constr_pattern in_or_out_modules
 | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
-| REPLACE "Search" searchabout_query searchabout_queries "."
-| WITH "Search" searchabout_queries
+| REPLACE "Search" search_query search_queries "."
+| WITH "Search" search_queries
 ]
 
 vernac_toplevel: [
@@ -1458,17 +1459,10 @@ ne_in_or_out_modules: [
 | DELETE "outside" LIST1 global
 ]
 
-searchabout_query: [
-| REPLACE positive_search_mark ne_string OPT scope_delimiter
-| WITH ne_string OPT scope_delimiter
-| REPLACE positive_search_mark constr_pattern
-| WITH constr_pattern
-]
-
-searchabout_queries: [
+search_queries: [
 | DELETE ne_in_or_out_modules
-| REPLACE searchabout_query searchabout_queries
-| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules
+| REPLACE search_query search_queries
+| WITH LIST1 ( search_query ) OPT ne_in_or_out_modules
 | DELETE (* empty *)
 ]
 
@@ -1476,6 +1470,27 @@ positive_search_mark: [
 | OPTINREF
 ]
 
+SPLICE: [
+| positive_search_mark
+]
+
+search_query: [
+| REPLACE OPT "-" search_item
+| WITH search_item
+| "-" search_query
+| REPLACE OPT "-" "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+| WITH "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+]
+
+search_item: [
+| REPLACE search_where ":" ne_string OPT scope_delimiter
+| WITH OPT ( search_where ":" ) ne_string OPT scope_delimiter
+| DELETE ne_string OPT scope_delimiter
+| REPLACE search_where ":" constr_pattern
+| WITH OPT ( search_where ":" ) constr_pattern
+| DELETE constr_pattern
+]
+
 by_notation: [
 | REPLACE ne_string OPT [ "%" IDENT ]
 | WITH ne_string OPT [ "%" scope_key ]
@@ -1631,7 +1646,6 @@ SPLICE: [
 | record_binder
 | at_level_opt
 | table_value
-| positive_search_mark
 | in_or_out_modules
 | option_setting
 | orient
@@ -1665,12 +1679,14 @@ SPLICE: [
 | intropatterns
 | instance_name
 | ne_in_or_out_modules
-| searchabout_queries
+| search_queries
 | locatable
 | scope_delimiter
 | bignat
 | one_import_filter_name
 | register_token
+| search_where
+| extended_def_token
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1719,7 +1735,9 @@ RENAME: [
 | record_binder_body field_body
 | class_rawexpr class
 | smart_global smart_qualid
+(*
 | searchabout_query search_item
+*)
 | option_table setting_name
 | argument_spec_block arg_specs
 | more_implicits_block implicits_alt
@@ -1729,8 +1747,6 @@ RENAME: [
 | numnotoption numeral_modifier
 ]
 
-(* todo: positive_search_mark is a lousy name for OPT "-" *)
-
 (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
 clause_dft_concl: [
 | OPTINREF
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 71d0251339..1b0a5c28ee 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1201,7 +1201,7 @@ query_command: [
 | "SearchHead" constr_pattern in_or_out_modules "."
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
-| "Search" searchabout_query searchabout_queries "."
+| "Search" search_query search_queries "."
 ]
 
 printable: [
@@ -1298,14 +1298,48 @@ positive_search_mark: [
 |
 ]
 
-searchabout_query: [
-| positive_search_mark ne_string OPT scope_delimiter
-| positive_search_mark constr_pattern
+search_query: [
+| positive_search_mark search_item
+| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
 ]
 
-searchabout_queries: [
+search_item: [
+| test_id_colon search_where ":" ne_string OPT scope_delimiter
+| "is" ":" logical_kind
+| ne_string OPT scope_delimiter
+| test_id_colon search_where ":" constr_pattern
+| constr_pattern
+]
+
+logical_kind: [
+| thm_token
+| assumption_token
+| "Context"
+| extended_def_token
+| "Primitive"
+]
+
+extended_def_token: [
+| def_token
+| "Coercion"
+| "Instance"
+| "Scheme"
+| "Canonical"
+| "Field"
+| "Method"
+]
+
+search_where: [
+| "head"
+| "hyp"
+| "concl"
+| "headhyp"
+| "headconcl"
+]
+
+search_queries: [
 | ne_in_or_out_modules
-| searchabout_query searchabout_queries
+| search_query search_queries
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3c85b65bca..3a327fc748 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -940,7 +940,7 @@ command: [
 | "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Time" sentence
 | "Redirect" string sentence
 | "Timeout" num sentence
@@ -996,9 +996,31 @@ comment: [
 | num
 ]
 
+search_query: [
+| search_item
+| "-" search_query
+| "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+]
+
 search_item: [
-| one_term
-| string OPT ( "%" scope_key )
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| "is" ":" logical_kind
+]
+
+logical_kind: [
+| thm_token
+| assumption_token
+| "Context"
+| "Definition"
+| "Example"
+| "Coercion"
+| "Instance"
+| "Scheme"
+| "Canonical"
+| "Field"
+| "Method"
+| "Primitive"
 ]
 
 univ_name_list: [