Merge PR #8855: More search options

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam

9 files changed, 374 insertions, 133 deletions

diff --git a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
new file mode 100644
index 0000000000..2fdacfd82a
--- /dev/null
+++ b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
@@ -0,0 +1,11 @@
+- **Changed:** The :cmd:`Search (ssreflect)` command that used to be
+  available when loading the `ssreflect` plugin has been moved to a
+  separate plugin that needs to be loaded separately: `ssrsearch`
+  (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes
+  `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo
+  Zimmermann).
+
+- **Deprecated:** :cmd:`Search (ssreflect)` (available through
+  `Require ssrsearch.`) in favor of the `headconcl:` clause of
+  :cmd:`Search` (part of `#8855
+  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
new file mode 100644
index 0000000000..cd993bf356
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
@@ -0,0 +1,9 @@
+- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`,
+  `headconcl:`, `head:` and `is:` in :cmd:`Search`.  Support for
+  complex search queries combining disjunctions, conjunctions and
+  negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo
+  Herbelin, with ideas from Cyril Cohen and help from Théo
+  Zimmermann).
+- **Deprecated:** :cmd:`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).
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 85481043b2..613669c34b 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 031abbe15c..3db9d2e80c 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/stdlib/hidden-files b/doc/stdlib/hidden-files
index 3af16cb731..0a9dba99a9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -91,3 +91,4 @@ theories/setoid_ring/Rings_Z.v
 theories/setoid_ring/ZArithRing.v
 theories/ssr/ssrunder.v
 theories/ssr/ssrsetoid.v
+theories/ssrsearch/ssrsearch.vo
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 62cc8ea86b..a9a243868f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -59,6 +59,8 @@ DELETE: [
 | lookup_at_as_comma
 | 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
@@ -1231,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: [
@@ -1457,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 *)
 ]
 
@@ -1475,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 ]
@@ -1485,14 +1501,6 @@ scope_delimiter: [
 | WITH "%" scope_key
 ]
 
-(* Don't show these details *)
-DELETE: [
-| register_token
-| register_prim_token
-| register_type_token
-]
-
-
 decl_notation: [
 | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ]
 | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ]
@@ -1638,7 +1646,6 @@ SPLICE: [
 | record_binder
 | at_level_opt
 | table_value
-| positive_search_mark
 | in_or_out_modules
 | option_setting
 | orient
@@ -1672,11 +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: [
@@ -1725,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
@@ -1735,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 92e9df51d5..1b0a5c28ee 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -798,58 +798,7 @@ gallina: [
 ]
 
 register_token: [
-| register_prim_token
-| register_type_token
-]
-
-register_type_token: [
-| "#int63_type"
-| "#float64_type"
-]
-
-register_prim_token: [
-| "#int63_head0"
-| "#int63_tail0"
-| "#int63_add"
-| "#int63_sub"
-| "#int63_mul"
-| "#int63_div"
-| "#int63_mod"
-| "#int63_lsr"
-| "#int63_lsl"
-| "#int63_land"
-| "#int63_lor"
-| "#int63_lxor"
-| "#int63_addc"
-| "#int63_subc"
-| "#int63_addcarryc"
-| "#int63_subcarryc"
-| "#int63_mulc"
-| "#int63_diveucl"
-| "#int63_div21"
-| "#int63_addmuldiv"
-| "#int63_eq"
-| "#int63_lt"
-| "#int63_le"
-| "#int63_compare"
-| "#float64_opp"
-| "#float64_abs"
-| "#float64_eq"
-| "#float64_lt"
-| "#float64_le"
-| "#float64_compare"
-| "#float64_classify"
-| "#float64_add"
-| "#float64_sub"
-| "#float64_mul"
-| "#float64_div"
-| "#float64_sqrt"
-| "#float64_of_int63"
-| "#float64_normfr_mantissa"
-| "#float64_frshiftexp"
-| "#float64_ldshiftexp"
-| "#float64_next_up"
-| "#float64_next_down"
+| test_hash_ident "#" IDENT
 ]
 
 thm_token: [
@@ -1252,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: [
@@ -1349,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
 |
 ]
 
@@ -1910,9 +1893,13 @@ debug: [
 |
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
+| "(" eauto_search_strategy_name ")"
 |
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 11f06b7b8a..3a327fc748 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -823,7 +823,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -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: [
@@ -1085,6 +1107,11 @@ hints_path: [
 | hints_path hints_path
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 class: [
 | "Funclass"
 | "Sortclass"