Merge PR #8855: More search options

Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
author: Emilio Jesus Gallego Arias 2020-05-16 19:21:05 +0200
committer: Emilio Jesus Gallego Arias 2020-05-16 19:21:05 +0200
commit: 2b0df4db404a1eb5b149e87ae0d23a5352b18f67 (patch)
tree: 0c127222b11fb7b8a32e1d9835cdc888b024364e
parent: 05e811a81de90ce698c4f0317d549dc01dc13e17 (diff)
parent: ca0002823429a6c7de953446b6d351332d24daa7 (diff)
36 files changed, 1340 insertions, 696 deletions
diff --git a/Makefile.common b/Makefile.common
index d435d7dfad..8f880e93fb 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -106,7 +106,7 @@ PLUGINDIRS:=\
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
-  ssrmatching	ltac		ssr
+  ssrmatching	ltac		ssr             ssrsearch
 
 USERCONTRIBDIRS:=\
 	Ltac2
@@ -158,6 +158,7 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
+SSRSEARCHCMO=plugins/ssrsearch/ssrsearch_plugin.cmo
 LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
 ZIFYCMO:=plugins/micromega/zify_plugin.cmo
 
@@ -166,7 +167,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(LTAC2CMO) $(ZIFYCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) $(SSRSEARCHCMO) $(LTAC2CMO) $(ZIFYCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
diff --git a/clib/cList.mli b/clib/cList.mli
index 07f42770f9..c8e471f989 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -265,7 +265,7 @@ sig
       This is the second part of [chop]. *)
 
   val skipn_at_least : int -> 'a list -> 'a list
-  (** Same as [skipn] but returns [] if [n] is larger than the list of
+  (** Same as [skipn] but returns [] if [n] is larger than the length of
       the list. *)
 
   val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
diff --git a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
new file mode 100644
index 0000000000..3b3b20baf1
--- /dev/null
+++ b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8855" ] || [ "$CI_BRANCH" = "master+more-search-options" ]; then
+
+    coqhammer_CI_REF=master+adapt-pr8855-search-api
+    coqhammer_CI_GITURL=https://github.com/herbelin/coqhammer
+
+    coq_dpdgraph_CI_REF=coq-master+adapt-pr8855-search-api
+    coq_dpdgraph_CI_GITURL=https://github.com/herbelin/coq-dpdgraph
+
+fi
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"
diff --git a/ide/idetop.ml b/ide/idetop.ml
index fa458e7c6e..bd99cbed1b 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -341,7 +341,10 @@ let import_search_constraint = function
 
 let search flags =
   let pstate = Vernacstate.Declare.get_pstate () in
-  List.map export_coq_object (Search.interface_search ?pstate (
+  let sigma, env = match pstate with
+  | None -> let env = Global.env () in Evd.(from_env env, env)
+  | Some p -> Declare.get_goal_context p 1 in
+  List.map export_coq_object (Search.interface_search env sigma (
     List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
   )
   [@@ocaml.warning "-3"]
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 14e5a81308..be1e3f05d2 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -49,3 +49,4 @@ val type_of_global_ref : Names.GlobRef.t -> string
 
 (** Registration of constant information *)
 val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit
+val constant_kind : Names.Constant.t -> Decls.logical_kind
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 4b78e64d98..7ef3e44848 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -15,7 +15,6 @@
 open Names
 module CoqConstr = Constr
 open CoqConstr
-open Termops
 open Constrexpr
 open Constrexpr_ops
 open Pcoq
@@ -23,8 +22,6 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
 open Ltac_plugin
-open Notation_ops
-open Notation_term
 open Glob_term
 open Stdarg
 open Pp
@@ -32,10 +29,8 @@ open Ppconstr
 open Printer
 open Util
 open Extraargs
-open Evar_kinds
 open Ssrprinters
 open Ssrcommon
-open Ssrparser
 
 }
 
@@ -129,7 +124,7 @@ GRAMMAR EXTEND Gram
   ] ];
 END
 
-(** Vernacular commands: Prenex Implicits and Search *)(***********************)
+(** Vernacular commands: Prenex Implicits *)
 
 (* This should really be implemented as an extension to the implicit   *)
 (* arguments feature, but unfortuately that API is sealed. The current *)
@@ -187,298 +182,6 @@ GRAMMAR EXTEND Gram
   ;
 END
 
-(** Extend Search to subsume SearchAbout, also adding hidden Type coercions. *)
-
-(* Main prefilter *)
-
-{
-
-type raw_glob_search_about_item =
-  | RGlobSearchSubPattern of constr_expr
-  | RGlobSearchString of Loc.t * string * string option
-
-let pr_search_item env sigma = function
-  | RGlobSearchString (_,s,_) -> str s
-  | RGlobSearchSubPattern p -> pr_constr_expr env sigma p
-
-let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item
-
-let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma
-
-(* Workaround the notation API that can only print notations *)
-
-let is_ident s = try CLexer.check_ident s; true with _ -> false
-
-let is_ident_part s = is_ident ("H" ^ s)
-
-let interp_search_notation ?loc tag okey =
-  let err msg = CErrors.user_err ?loc ~hdr:"interp_search_notation" msg in
-  let mk_pntn s for_key =
-    let n = String.length s in
-    let s' = Bytes.make (n + 2) ' ' in
-    let rec loop i i' =
-      if i >= n then s', i' - 2 else if s.[i] = ' ' then loop (i + 1) i' else
-      let j = try String.index_from s (i + 1) ' ' with _ -> n in
-      let m = j - i in
-      if s.[i] = '\'' && i < j - 2 && s.[j - 1] = '\'' then
-        (String.blit s (i + 1) s' i' (m - 2); loop (j + 1) (i' + m - 1))
-      else if for_key && is_ident (String.sub s i m) then
-         (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
-      else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
-    loop 0 1 in
-  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
-  let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
-  let pr_and_list pr = function
-    | [x] -> pr x
-    | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
-    | [] -> mt () in
-  let pr_sc sc = str (if sc = "" then "independently" else sc) in
-  let pr_scs = function
-    | [""] -> pr_sc ""
-    | scs -> str "in " ++ pr_and_list pr_sc scs in
-  let generator, pr_tag_sc =
-    let ign _ = mt () in match okey with
-  | Some key ->
-    let sc = Notation.find_delimiters_scope ?loc key in
-    let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in
-    Notation.pr_scope ign sc, pr_sc
-  | None -> Notation.pr_scopes ign, ign in
-  let qtag s_in = pr_tag_sc s_in ++ qstring tag ++ spc()in
-  let ptag, ttag =
-    let ptag, m = mk_pntn tag false in
-    if m <= 0 then err (str "empty notation fragment");
-    ptag, trim_ntn (ptag, m) in
-  let last = ref "" and last_sc = ref "" in
-  let scs = ref [] and ntns = ref [] in
-  let push_sc sc = match !scs with
-  | "" :: scs' ->  scs := "" :: sc :: scs'
-  | scs' -> scs := sc :: scs' in
-  let get s _ _ = match !last with
-  | "Scope " -> last_sc := s; last := ""
-  | "Lonely notation" -> last_sc := ""; last := ""
-  | "\"" ->
-      let pntn, m = mk_pntn s true in
-      if String.string_contains ~where:(Bytes.to_string pntn) ~what:(Bytes.to_string ptag) then begin
-        let ntn = trim_ntn (pntn, m) in
-        match !ntns with
-        | [] -> ntns := [ntn]; scs := [!last_sc]
-        | ntn' :: _ when ntn' = ntn -> push_sc !last_sc
-        | _ when ntn = ttag -> ntns := ntn :: !ntns; scs := [!last_sc]
-        | _ :: ntns' when List.mem ntn ntns' -> ()
-        | ntn' :: ntns' -> ntns := ntn' :: ntn :: ntns'
-      end;
-      last := ""
-  | _ -> last := s in
-  pp_with (Format.make_formatter get (fun _ -> ())) generator;
-  let ntn = match !ntns with
-  | [] ->
-    err (hov 0 (qtag "in" ++ str "does not occur in any notation"))
-  | ntn :: ntns' when ntn = ttag ->
-    if ntns' <> [] then begin
-      let pr_ntns' = pr_and_list pr_ntn ntns' in
-      Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
-    end; ntn
-  | [ntn] ->
-    Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
-  | ntns' ->
-    let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
-    err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
-  let (nvars, body), ((_, pat), osc) = match !scs with
-  | [sc] -> Notation.interp_notation ?loc ntn (None, [sc])
-  | scs' ->
-    try Notation.interp_notation ?loc ntn (None, []) with _ ->
-    let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in
-    err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in
-  let sc = Option.default "" osc in
-  let _ =
-    let m_sc =
-      if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in
-    let ntn_pat = trim_ntn (mk_pntn pat false) in
-    let rbody = glob_constr_of_notation_constr ?loc body in
-    let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
-    let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
-    Feedback.msg_notice (hov 0 m) in
-  if List.length !scs > 1 then
-    let scs' = List.remove (=) sc !scs in
-    let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
-    Feedback.msg_warning (hov 4 w)
-  else if String.string_contains ~where:(snd ntn) ~what:" .. " then
-    err (pr_ntn ntn ++ str " is an n-ary notation");
-  let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
-  let rec sub () = function
-  | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
-  | c ->
-    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
-  let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
-  Search.GlobSearchSubPattern npat
-
-}
-
-ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem
-  PRINTED BY { pr_ssr_search_item env sigma }
-  | [ string(s) ] -> {  RGlobSearchString (loc,s,None)  }
-  | [ string(s) "%" preident(key) ] -> {  RGlobSearchString (loc,s,Some key)  }
-  | [ constr_pattern(p) ] -> {  RGlobSearchSubPattern p  }
-END
-
-{
-
-let pr_ssr_search_arg env sigma _ _ _ =
-  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in
-  pr_list spc pr_item
-
-}
-
-ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list
-  PRINTED BY { pr_ssr_search_arg env sigma }
-  | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> {  (false, p) :: a  }
-  | [ ssr_search_item(p) ssr_search_arg(a) ] -> {  (true, p) :: a  }
-  | [ ] -> {  []  }
-END
-
-{
-
-(* Main type conclusion pattern filter *)
-
-let rec splay_search_pattern na = function
-  | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp
-  | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp
-  | Pattern.PRef hr -> hr, na
-  | _ -> CErrors.user_err (Pp.str "no head constant in head search pattern")
-
-let push_rels_assum l e =
-  let l = List.map (fun (n,t) -> n, EConstr.Unsafe.to_constr t) l in
-  push_rels_assum l e
-
-let coerce_search_pattern_to_sort hpat =
-  let env = Global.env () in
-  let sigma = Evd.(from_env env) in
-  let mkPApp fp n_imps args =
-    let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in
-    Pattern.PApp (fp, args') in
-  let hr, na = splay_search_pattern 0 hpat in
-  let dc, ht =
-    let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in
-    Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
-  let np = List.length dc in
-  if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
-  let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
-  let warn () =
-    Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++
-      pr_constr_pattern_env env sigma hpat') in
-  if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
-  let filter_head, coe_path =
-    try
-      let _, cp =
-        Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
-      warn ();
-      true, cp
-    with _ -> false, [] in
-  let coerce hp coe_index =
-    let coe_ref = coe_index.Coercionops.coe_value in
-    try
-      let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in
-      mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
-    with Not_found | Option.IsNone ->
-    errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
-            ++ str "to interpret head search pattern as type") in
-  filter_head, List.fold_left coerce hpat' coe_path
-
-let interp_head_pat hpat =
-  let filter_head, p = coerce_search_pattern_to_sort hpat in
-  let rec loop c = match CoqConstr.kind c with
-  | Cast (c', _, _) -> loop c'
-  | Prod (_, _, c') -> loop c'
-  | LetIn (_, _, _, c') -> loop c'
-  | _ ->
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
-  filter_head, loop
-
-let all_true _ = true
-
-let rec interp_search_about args accu = match args with
-| [] -> accu
-| (flag, arg) :: rem ->
-  fun gr env typ ->
-    let ans = Search.search_filter arg gr env typ in
-    (if flag then ans else not ans) && interp_search_about rem accu gr env typ
-
-let interp_search_arg arg =
-  let arg = List.map (fun (x,arg) -> x, match arg with
-  | RGlobSearchString (loc,s,key) ->
-      if is_ident_part s then Search.GlobSearchString s else
-      interp_search_notation ~loc s key
-  | RGlobSearchSubPattern p ->
-    let env = Global.env () in
-    let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
-    Search.GlobSearchSubPattern p) arg
-  in
-  let hpat, a1 = match arg with
-  | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a'
-  | (true, Search.GlobSearchSubPattern p) :: a' ->
-     let filter_head, p = interp_head_pat p in
-     if filter_head then p, a' else all_true, arg
-  | _ -> all_true, arg in
-  let is_string =
-    function (_, Search.GlobSearchString _) -> true | _ -> false in
-  let a2, a3 = List.partition is_string a1 in
-  interp_search_about (a2 @ a3) (fun gr env typ -> hpat typ)
-
-(* Module path postfilter *)
-
-let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
-
-let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc)
-
-let pr_ssr_modlocs _ _ _ ml =
-  if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml
-
-}
-
-ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY { pr_ssr_modlocs }
-  | [ ] -> {  []  }
-END
-
-GRAMMAR EXTEND Gram
-  GLOBAL: ssr_modlocs;
-  modloc: [[ "-"; m = global -> { true, m } | m = global -> { false, m } ]];
-  ssr_modlocs: [[ "in"; ml = LIST1 modloc -> { ml } ]];
-END
-
-{
-
-let interp_modloc mr =
-  let interp_mod (_, qid) =
-    try Nametab.full_name_module qid with Not_found ->
-    CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
-  let mr_out, mr_in = List.partition fst mr in
-  let interp_bmod b = function
-  | [] -> fun _ _ _ -> true
-  | rmods -> Search.module_filter (List.map interp_mod rmods, b) in
-  let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in
-  fun gr env typ -> is_in gr env typ && is_out gr env typ
-
-(* The unified, extended vernacular "Search" command *)
-
-let ssrdisplaysearch gr env t =
-  let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
-  Feedback.msg_notice (hov 2 pr_res ++ fnl ())
-
-}
-
-VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
-| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] ->
-  { let hpat = interp_search_arg a in
-    let in_mod = interp_modloc mr in
-    let post_filter gr env typ = in_mod gr env typ && hpat gr env typ in
-    let display gr env typ =
-      if post_filter gr env typ then ssrdisplaysearch gr env typ
-    in
-    Search.generic_search None display }
-END
-
 (** View hint database and View application. *)(* ******************************)
 
 (* There are three databases of lemmas used to mediate the application  *)
diff --git a/plugins/ssrsearch/dune b/plugins/ssrsearch/dune
new file mode 100644
index 0000000000..2851835eae
--- /dev/null
+++ b/plugins/ssrsearch/dune
@@ -0,0 +1,7 @@
+(library
+ (name ssrsearch_plugin)
+ (public_name coq.plugins.ssrsearch)
+ (synopsis "Deprecated Search command from SSReflect")
+ (libraries coq.plugins.ssreflect))
+
+(coq.pp (modules g_search))
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
new file mode 100644
index 0000000000..1651e1cc71
--- /dev/null
+++ b/plugins/ssrsearch/g_search.mlg
@@ -0,0 +1,321 @@
+(** Extend Search to subsume SearchAbout, also adding hidden Type coercions. *)
+
+(* Main prefilter *)
+
+{
+
+module CoqConstr = Constr
+open CoqConstr
+open Constrexpr
+open Evar_kinds
+open Glob_term
+open Ltac_plugin
+open Notation_ops
+open Notation_term
+open Pcoq.Prim
+open Pcoq.Constr
+open Pp
+open Ppconstr
+open Printer
+open Stdarg
+open Ssreflect_plugin.Ssrprinters
+open Ssreflect_plugin.Ssrcommon
+open Ssreflect_plugin.Ssrparser
+open Termops
+open Util
+
+type raw_glob_search_about_item =
+  | RGlobSearchSubPattern of constr_expr
+  | RGlobSearchString of Loc.t * string * string option
+
+let pr_search_item env sigma = function
+  | RGlobSearchString (_,s,_) -> str s
+  | RGlobSearchSubPattern p -> pr_constr_expr env sigma p
+
+let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item
+
+let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma
+
+(* Workaround the notation API that can only print notations *)
+
+let is_ident s = try CLexer.check_ident s; true with _ -> false
+
+let is_ident_part s = is_ident ("H" ^ s)
+
+let interp_search_notation ?loc tag okey =
+  let err msg = CErrors.user_err ?loc ~hdr:"interp_search_notation" msg in
+  let mk_pntn s for_key =
+    let n = String.length s in
+    let s' = Bytes.make (n + 2) ' ' in
+    let rec loop i i' =
+      if i >= n then s', i' - 2 else if s.[i] = ' ' then loop (i + 1) i' else
+      let j = try String.index_from s (i + 1) ' ' with _ -> n in
+      let m = j - i in
+      if s.[i] = '\'' && i < j - 2 && s.[j - 1] = '\'' then
+        (String.blit s (i + 1) s' i' (m - 2); loop (j + 1) (i' + m - 1))
+      else if for_key && is_ident (String.sub s i m) then
+         (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
+      else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
+    loop 0 1 in
+  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
+  let pr_and_list pr = function
+    | [x] -> pr x
+    | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
+    | [] -> mt () in
+  let pr_sc sc = str (if sc = "" then "independently" else sc) in
+  let pr_scs = function
+    | [""] -> pr_sc ""
+    | scs -> str "in " ++ pr_and_list pr_sc scs in
+  let generator, pr_tag_sc =
+    let ign _ = mt () in match okey with
+  | Some key ->
+    let sc = Notation.find_delimiters_scope ?loc key in
+    let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in
+    Notation.pr_scope ign sc, pr_sc
+  | None -> Notation.pr_scopes ign, ign in
+  let qtag s_in = pr_tag_sc s_in ++ qstring tag ++ spc()in
+  let ptag, ttag =
+    let ptag, m = mk_pntn tag false in
+    if m <= 0 then err (str "empty notation fragment");
+    ptag, trim_ntn (ptag, m) in
+  let last = ref "" and last_sc = ref "" in
+  let scs = ref [] and ntns = ref [] in
+  let push_sc sc = match !scs with
+  | "" :: scs' ->  scs := "" :: sc :: scs'
+  | scs' -> scs := sc :: scs' in
+  let get s _ _ = match !last with
+  | "Scope " -> last_sc := s; last := ""
+  | "Lonely notation" -> last_sc := ""; last := ""
+  | "\"" ->
+      let pntn, m = mk_pntn s true in
+      if String.string_contains ~where:(Bytes.to_string pntn) ~what:(Bytes.to_string ptag) then begin
+        let ntn = trim_ntn (pntn, m) in
+        match !ntns with
+        | [] -> ntns := [ntn]; scs := [!last_sc]
+        | ntn' :: _ when ntn' = ntn -> push_sc !last_sc
+        | _ when ntn = ttag -> ntns := ntn :: !ntns; scs := [!last_sc]
+        | _ :: ntns' when List.mem ntn ntns' -> ()
+        | ntn' :: ntns' -> ntns := ntn' :: ntn :: ntns'
+      end;
+      last := ""
+  | _ -> last := s in
+  pp_with (Format.make_formatter get (fun _ -> ())) generator;
+  let ntn = match !ntns with
+  | [] ->
+    err (hov 0 (qtag "in" ++ str "does not occur in any notation"))
+  | ntn :: ntns' when ntn = ttag ->
+    if ntns' <> [] then begin
+      let pr_ntns' = pr_and_list pr_ntn ntns' in
+      Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
+    end; ntn
+  | [ntn] ->
+    Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+  | ntns' ->
+    let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
+    err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
+  let (nvars, body), ((_, pat), osc) = match !scs with
+  | [sc] -> Notation.interp_notation ?loc ntn (None, [sc])
+  | scs' ->
+    try Notation.interp_notation ?loc ntn (None, []) with _ ->
+    let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in
+    err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in
+  let sc = Option.default "" osc in
+  let _ =
+    let m_sc =
+      if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in
+    let ntn_pat = trim_ntn (mk_pntn pat false) in
+    let rbody = glob_constr_of_notation_constr ?loc body in
+    let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
+    let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
+    Feedback.msg_notice (hov 0 m) in
+  if List.length !scs > 1 then
+    let scs' = List.remove (=) sc !scs in
+    let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
+    Feedback.msg_warning (hov 4 w)
+  else if String.string_contains ~where:(snd ntn) ~what:" .. " then
+    err (pr_ntn ntn ++ str " is an n-ary notation");
+  let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
+  let rec sub () = function
+  | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
+  | c ->
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
+  let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
+  Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
+
+}
+
+ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem
+  PRINTED BY { pr_ssr_search_item env sigma }
+  | [ string(s) ] -> {  RGlobSearchString (loc,s,None)  }
+  | [ string(s) "%" preident(key) ] -> {  RGlobSearchString (loc,s,Some key)  }
+  | [ constr_pattern(p) ] -> {  RGlobSearchSubPattern p  }
+END
+
+{
+
+let pr_ssr_search_arg env sigma _ _ _ =
+  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in
+  pr_list spc pr_item
+
+}
+
+ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list
+  PRINTED BY { pr_ssr_search_arg env sigma }
+  | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> {  (false, p) :: a  }
+  | [ ssr_search_item(p) ssr_search_arg(a) ] -> {  (true, p) :: a  }
+  | [ ] -> {  []  }
+END
+
+{
+
+(* Main type conclusion pattern filter *)
+
+let rec splay_search_pattern na = function
+  | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp
+  | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp
+  | Pattern.PRef hr -> hr, na
+  | _ -> CErrors.user_err (Pp.str "no head constant in head search pattern")
+
+let push_rels_assum l e =
+  let l = List.map (fun (n,t) -> n, EConstr.Unsafe.to_constr t) l in
+  push_rels_assum l e
+
+let coerce_search_pattern_to_sort hpat =
+  let env = Global.env () in
+  let sigma = Evd.(from_env env) in
+  let mkPApp fp n_imps args =
+    let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in
+    Pattern.PApp (fp, args') in
+  let hr, na = splay_search_pattern 0 hpat in
+  let dc, ht =
+    let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in
+    Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
+  let np = List.length dc in
+  if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
+  let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
+  let warn () =
+    Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++
+      pr_constr_pattern_env env sigma hpat') in
+  if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
+  let filter_head, coe_path =
+    try
+      let _, cp =
+        Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in
+      warn ();
+      true, cp
+    with _ -> false, [] in
+  let coerce hp coe_index =
+    let coe_ref = coe_index.Coercionops.coe_value in
+    try
+      let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in
+      mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
+    with Not_found | Option.IsNone ->
+    errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
+            ++ str "to interpret head search pattern as type") in
+  filter_head, List.fold_left coerce hpat' coe_path
+
+let interp_head_pat hpat =
+  let filter_head, p = coerce_search_pattern_to_sort hpat in
+  let rec loop c = match CoqConstr.kind c with
+  | Cast (c', _, _) -> loop c'
+  | Prod (_, _, c') -> loop c'
+  | LetIn (_, _, _, c') -> loop c'
+  | _ ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
+  filter_head, loop
+
+let all_true _ = true
+
+let rec interp_search_about args accu = match args with
+| [] -> accu
+| (flag, arg) :: rem ->
+  fun gr kind env typ ->
+    let ans = Search.search_filter arg gr kind env (Evd.from_env env) typ in
+    (if flag then ans else not ans) && interp_search_about rem accu gr kind env typ
+
+let interp_search_arg arg =
+  let arg = List.map (fun (x,arg) -> x, match arg with
+  | RGlobSearchString (loc,s,key) ->
+      if is_ident_part s then Search.GlobSearchString s else
+      interp_search_notation ~loc s key
+  | RGlobSearchSubPattern p ->
+    let env = Global.env () in
+    let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
+    Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,p)) arg
+  in
+  let hpat, a1 = match arg with
+  | (_, Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,Pattern.PMeta _)) :: a' -> all_true, a'
+  | (true, Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,p)) :: a' ->
+     let filter_head, p = interp_head_pat p in
+     if filter_head then p, a' else all_true, arg
+  | (_, (Search.GlobSearchSubPattern (Vernacexpr.(InHyp|InConcl),_,_)
+        |Search.GlobSearchSubPattern (Vernacexpr.Anywhere,true,_))) :: a' -> CErrors.user_err (str "Unsupported.")
+  | _ -> all_true, arg in
+  let is_string =
+    function (_, Search.GlobSearchString _) -> true | _ -> false in
+  let a2, a3 = List.partition is_string a1 in
+  interp_search_about (a2 @ a3) (fun gr kind env typ -> hpat typ)
+
+(* Module path postfilter *)
+
+let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
+
+let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc)
+
+let pr_ssr_modlocs _ _ _ ml =
+  if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml
+
+}
+
+ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY { pr_ssr_modlocs }
+  | [ ] -> {  []  }
+END
+
+GRAMMAR EXTEND Gram
+  GLOBAL: ssr_modlocs;
+  modloc: [[ "-"; m = global -> { true, m } | m = global -> { false, m } ]];
+  ssr_modlocs: [[ "in"; ml = LIST1 modloc -> { ml } ]];
+END
+
+{
+
+let interp_modloc mr =
+  let interp_mod (_, qid) =
+    try Nametab.full_name_module qid with Not_found ->
+    CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
+  let mr_out, mr_in = List.partition fst mr in
+  let interp_bmod b = function
+  | [] -> fun _ _ _ _ _ -> true
+  | rmods -> Search.module_filter (List.map interp_mod rmods, b) in
+  let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in
+  fun gr kind env typ -> is_in gr kind env (Evd.from_env env) typ && is_out gr kind env (Evd.from_env env) typ
+
+(* The unified, extended vernacular "Search" command *)
+
+let ssrdisplaysearch gr env t =
+  let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
+  Feedback.msg_notice (hov 2 pr_res ++ fnl ())
+
+let deprecated_search =
+  CWarnings.create
+    ~name:"deprecated-ssr-search"
+    ~category:"deprecated"
+    (fun () -> Pp.(str"SSReflect's Search command is deprecated."))
+
+}
+
+VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY
+| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] ->
+  { deprecated_search ();
+    let hpat = interp_search_arg a in
+    let in_mod = interp_modloc mr in
+    let post_filter gr kind env typ = in_mod gr kind env typ && hpat gr kind env typ in
+    let display gr kind env typ =
+      if post_filter gr kind env typ then ssrdisplaysearch gr env typ
+    in
+    let env = Global.env () in
+    Search.generic_search env display }
+END
diff --git a/plugins/ssrsearch/ssrsearch_plugin.mlpack b/plugins/ssrsearch/ssrsearch_plugin.mlpack
new file mode 100644
index 0000000000..0c32130d65
--- /dev/null
+++ b/plugins/ssrsearch/ssrsearch_plugin.mlpack
@@ -0,0 +1 @@
+G_search
diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml
index 84fa1ee508..f7fe595df5 100644
--- a/tactics/declareScheme.ml
+++ b/tactics/declareScheme.ml
@@ -40,3 +40,5 @@ let declare_scheme kind indcl =
   Lib.add_anonymous_leaf (inScheme (kind,indcl))
 
 let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map)
+
+let all_schemes () = Indmap.domain !scheme_map
diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli
index 5a771009bd..d10cb4ef15 100644
--- a/tactics/declareScheme.mli
+++ b/tactics/declareScheme.mli
@@ -10,3 +10,4 @@
 
 val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit
 val lookup_scheme : string -> Names.inductive -> Names.Constant.t
+val all_schemes : unit -> Names.Indset.t
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c01f4b2e19..317e9c3757 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -18,7 +18,6 @@ le_sind:
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
-(use "About" for full details on implicit arguments)
 false: bool
 true: bool
 is_true: bool -> Prop
@@ -136,7 +135,6 @@ bool_choice:
   forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-(use "About" for full details on implicit arguments)
 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
@@ -162,7 +160,6 @@ f_equal2_mult:
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-(use "About" for full details on implicit arguments)
 Numeral.internal_numeral_dec_lb:
   forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
 Numeral.internal_int_dec_lb1:
@@ -216,7 +213,6 @@ bool_choice:
   forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-(use "About" for full details on implicit arguments)
 Numeral.internal_numeral_dec_lb:
   forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
 Numeral.internal_numeral_dec_bl:
@@ -266,23 +262,15 @@ Hexadecimal.internal_uint_dec_lb0:
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-(use "About" for full details on implicit arguments)
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
 h': newdef n <> n
-(use "About" for full details on implicit arguments)
-(use "About" for full details on implicit arguments)
 The command has indeed failed with message:
 [Focus] No such goal.
 The command has indeed failed with message:
@@ -291,14 +279,179 @@ The command has indeed failed with message:
 Query commands only support the single numbered goal selector.
 h: P n
 h': ~ P n
-(use "About" for full details on implicit arguments)
 h: P n
 h': ~ P n
-(use "About" for full details on implicit arguments)
 h: P n
 h': ~ P n
-(use "About" for full details on implicit arguments)
 h: P n
-(use "About" for full details on implicit arguments)
 h: P n
-(use "About" for full details on implicit arguments)
+a: A
+b: A
+or_assoc: forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C
+and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
+eq_trans_assoc:
+  forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t),
+  eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+nat_rect_plus:
+  forall (n m : nat) {A : Type} (f : A -> A) (x : A),
+  nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) =
+  nat_rect (fun _ : nat => A)
+    (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) 
+    (fun _ : nat => f) n
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+Numeral.internal_numeral_dec_bl:
+  forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y
+Numeral.internal_int_dec_bl1:
+  forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y
+Numeral.internal_uint_dec_bl1:
+  forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Hexadecimal.internal_int_dec_bl0:
+  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Decimal.internal_int_dec_bl:
+  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
+Byte.of_bits:
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
+  Byte.byte
+Byte.to_bits_of_bits:
+  forall
+    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
+  Byte.to_bits (Byte.of_bits b) = b
+Numeral.internal_numeral_dec_lb:
+  forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true
+Numeral.internal_uint_dec_lb1:
+  forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true
+Numeral.internal_int_dec_lb1:
+  forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true
+Decimal.internal_int_dec_lb:
+  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
+Hexadecimal.internal_hexadecimal_dec_lb:
+  forall x y : Hexadecimal.hexadecimal,
+  x = y -> Hexadecimal.hexadecimal_beq x y = true
+Hexadecimal.internal_int_dec_lb0:
+  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
+Decimal.internal_decimal_dec_lb:
+  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Hexadecimal.internal_uint_dec_bl0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_lb:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
+Hexadecimal.internal_uint_dec_lb0:
+  forall x : Hexadecimal.uint,
+  (fun x0 : Hexadecimal.uint =>
+   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+Byte.to_bits_of_bits:
+  forall
+    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
+  Byte.to_bits (Byte.of_bits b) = b
+bool_choice:
+  forall [S : Set] [R1 R2 : S -> Prop],
+  (forall x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+Nat.two: nat
+Nat.zero: nat
+Nat.one: nat
+Nat.succ: nat -> nat
+Nat.log2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.square: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.of_hex_uint: Hexadecimal.uint -> nat
+Nat.of_uint: Decimal.uint -> nat
+Nat.of_num_uint: Numeral.uint -> nat
+length: forall [A : Type], list A -> nat
+plus_n_O: forall n : nat, n = n + 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a
+Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a
+Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a
+Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a
+Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n
+Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n
+Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b
+Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n
+Nat.mul_comm: forall n m : nat, n * m = m * n
+Nat.add_comm: forall n m : nat, n + m = m + n
+Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool
+Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool
+Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
+Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
+Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
+Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
+Nat.testbit_spec':
+  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
+Nat.pow_div_l:
+  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
+Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
+Nat.testbit_false:
+  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
+Nat.testbit_true:
+  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
+Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
+Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
+Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
+Nat.testbit_spec':
+  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
+Nat.pow_div_l:
+  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
+Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
+Nat.testbit_false:
+  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
+Nat.testbit_true:
+  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
+iff_Symmetric: Symmetric iff
+iff_Reflexive: Reflexive iff
+impl_Reflexive: Reflexive Basics.impl
+eq_Symmetric: forall {A : Type}, Symmetric eq
+eq_Reflexive: forall {A : Type}, Reflexive eq
+Equivalence_Symmetric:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  Equivalence R -> Symmetric R
+Equivalence_Reflexive:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  Equivalence R -> Reflexive R
+PER_Symmetric:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  PER R -> Symmetric R
+PreOrder_Reflexive:
+  forall {A : Type} {R : Relation_Definitions.relation A},
+  PreOrder R -> Reflexive R
+reflexive_eq_dom_reflexive:
+  forall {A B : Type} {R' : Relation_Definitions.relation B},
+  Reflexive R' -> Reflexive (eq ==> R')%signature
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 82096f29bf..4ec7a760b9 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -35,3 +35,34 @@ Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
 
 Abort.
 
+Module M.
+Section S.
+Variable A:Type.
+Variable a:A.
+Theorem Thm (b:A) : True.
+Search A. (* Test search in hypotheses *)
+Abort.
+End S.
+End M.
+
+(* Reproduce the example of the doc *)
+
+Reset Initial.
+
+Search "_assoc".
+Search "+".
+Search hyp:bool -headhyp:bool.
+Search concl:bool -headconcl:bool.
+Search [ is:Definition headconcl:nat | is:Lemma (_ + _) ].
+
+Require Import PeanoNat.
+
+Search (_ ?n ?m = _ ?m ?n).
+Search "'mod'" -"mod".
+Search "mod"%nat -"mod".
+
+Reset Initial.
+
+Require Import Morphisms.
+
+Search is:Instance [ Reflexive | Symmetric ].
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index d42dc575c2..9554581ebe 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,10 +1,17 @@
+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
-(use "About" for full details on implicit arguments)
+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
@@ -28,7 +35,10 @@ 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
-(use "About" for full details on implicit arguments)
+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
@@ -47,8 +57,13 @@ 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
-(use "About" for full details on implicit arguments)
+File "stdin", line 11, characters 2-20:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 h: newdef n
-(use "About" for full details on implicit arguments)
+File "stdin", line 17, characters 2-15:
+Warning:
+SearchHead is deprecated. Use the headconcl: clause of Search instead.
+[deprecated-searchhead,deprecated]
 h: P n
-(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 13d0a9e55b..80b03e8a0b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -21,7 +21,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
-(use "About" for full details on implicit arguments)
 Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
@@ -61,8 +60,6 @@ Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 length: forall [A : Type], list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-(use "About" for full details on implicit arguments)
-(use "About" for full details on implicit arguments)
 Nat.div2: nat -> nat
 Nat.sqrt: nat -> nat
 Nat.log2: nat -> nat
@@ -92,29 +89,19 @@ Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-(use "About" for full details on implicit arguments)
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-(use "About" for full details on implicit arguments)
 iff_refl: forall A : Prop, A <-> A
 le_n: forall n : nat, n <= n
 identity_refl: forall [A : Type] (a : A), identity a a
 eq_refl: forall {A : Type} {x : A}, x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-(use "About" for full details on implicit arguments)
+(use "About" for full details on the implicit arguments of eq_refl)
 conj: forall [A B : Prop], A -> B -> A /\ B
 pair: forall {A B : Type}, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-(use "About" for full details on implicit arguments)
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
-(use "About" for full details on implicit arguments)
 h: n <> newdef n
-(use "About" for full details on implicit arguments)
 h: P n
-(use "About" for full details on implicit arguments)
 h': ~ P n
-(use "About" for full details on implicit arguments)
 h: P n
-(use "About" for full details on implicit arguments)
 h: P n
-(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out
index 3c0880b20c..5edea5dff6 100644
--- a/test-suite/output/SearchRewrite.out
+++ b/test-suite/output/SearchRewrite.out
@@ -1,10 +1,5 @@
 plus_n_O: forall n : nat, n = n + 0
-(use "About" for full details on implicit arguments)
 plus_O_n: forall n : nat, 0 + n = n
-(use "About" for full details on implicit arguments)
 h: n = newdef n
-(use "About" for full details on implicit arguments)
 h: n = newdef n
-(use "About" for full details on implicit arguments)
 h: n = newdef n
-(use "About" for full details on implicit arguments)
diff --git a/theories/dune b/theories/dune
index b9af76d699..de8dcdc5b1 100644
--- a/theories/dune
+++ b/theories/dune
@@ -33,6 +33,7 @@
    coq.plugins.funind
 
    coq.plugins.ssreflect
+   coq.plugins.ssrsearch
    coq.plugins.derive))
 
 (include_subdirs qualified)
diff --git a/theories/ssrsearch/ssrsearch.v b/theories/ssrsearch/ssrsearch.v
new file mode 100644
index 0000000000..37ab8f4bac
--- /dev/null
+++ b/theories/ssrsearch/ssrsearch.v
@@ -0,0 +1,2 @@
+Require Import ssreflect.
+Declare ML Module "ssrsearch_plugin".
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
new file mode 100644
index 0000000000..9de8d6fbc3
--- /dev/null
+++ b/vernac/comSearch.ml
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Interpretation of search commands *)
+
+open CErrors
+open Names
+open Util
+open Pp
+open Printer
+open Search
+open Vernacexpr
+open Goptions
+
+let global_module qid =
+  try Nametab.full_name_module qid
+  with Not_found ->
+    user_err ?loc:qid.CAst.loc ~hdr:"global_module"
+     (str "Module/section " ++ Ppconstr.pr_qualid qid ++ str " not found.")
+
+let interp_search_restriction = function
+  | SearchOutside l -> (List.map global_module l, true)
+  | SearchInside l -> (List.map global_module l, false)
+
+let kind_searcher = Decls.(function
+  (* Kinds referring to the keyword introducing the object *)
+  | IsAssumption _
+  | IsDefinition (Definition | Example | Fixpoint | CoFixpoint | Method | StructureComponent | Let)
+  | IsProof _
+  | IsPrimitive as k -> Inl k
+  (* Kinds referring to the status of the object *)
+  | IsDefinition (Coercion | SubClass | IdentityCoercion as k') ->
+    let coercions = Coercionops.coercions () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr &&
+                                      (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions)
+  | IsDefinition CanonicalStructure ->
+    let canonproj = Recordops.canonical_projections () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj)
+  | IsDefinition Scheme ->
+    let schemes = DeclareScheme.all_schemes () in
+    Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes)
+  | IsDefinition Instance ->
+    let instances = Typeclasses.all_instances () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Typeclasses.is_impl gr) instances))
+
+let interp_search_item env sigma =
+  function
+  | SearchSubPattern ((where,head),pat) ->
+      let _,pat = Constrintern.intern_constr_pattern env sigma pat in
+      GlobSearchSubPattern (where,head,pat)
+  | SearchString ((Anywhere,false),s,None) when Id.is_valid s ->
+      GlobSearchString s
+  | SearchString ((where,head),s,sc) ->
+      (try
+        let ref =
+          Notation.interp_notation_as_global_reference
+            ~head:false (fun _ -> true) s sc in
+        GlobSearchSubPattern (where,head,Pattern.PRef ref)
+      with UserError _ ->
+        user_err ~hdr:"interp_search_item"
+          (str "Unable to interpret " ++ quote (str s) ++ str " as a reference."))
+  | SearchKind k ->
+     match kind_searcher k with
+     | Inl k -> GlobSearchKind k
+     | Inr f -> GlobSearchFilter f
+
+let rec interp_search_request env sigma = function
+  | b, SearchLiteral i -> b, GlobSearchLiteral (interp_search_item env sigma i)
+  | b, SearchDisjConj l -> b, GlobSearchDisjConj (List.map (List.map (interp_search_request env sigma)) l)
+
+(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
+   `search_output_name_only` option to avoid excessive printing when
+   searching.
+
+   The motivation was to make search usable for IDE completion,
+   however, it is still too slow due to the non-indexed nature of the
+   underlying search mechanism.
+
+   In the future we should deprecate the option and provide a fast,
+   indexed name-searching interface.
+*)
+let search_output_name_only = ref false
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
+      optkey   = ["Search";"Output";"Name";"Only"];
+      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
+  let warnlist = ref [] in
+  let pr_search ref kind env c =
+    let pr = pr_global ref in
+    let pp = if !search_output_name_only
+      then pr
+      else begin
+        let open Impargs in
+        let impls = implicits_of_global ref in
+        let impargs = select_stronger_impargs impls in
+        let impargs = List.map binding_kind_of_status impargs in
+        if List.length impls > 1 ||
+           List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true)
+             (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs)
+          then warnlist := pr :: !warnlist;
+        let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in
+        hov 2 (pr ++ str":" ++ spc () ++ pc)
+      end
+    in Feedback.msg_notice pp
+  in
+  (match s with
+  | SearchPattern c ->
+      (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);
+  if !warnlist <> [] then
+  Feedback.msg_notice (str "(" ++
+    hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++
+           pr_enum (fun x -> x) !warnlist ++ str ")"))
diff --git a/vernac/comSearch.mli b/vernac/comSearch.mli
new file mode 100644
index 0000000000..42f59984ff
--- /dev/null
+++ b/vernac/comSearch.mli
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Interpretation of search commands *)
+
+val interp_search : Environ.env -> Evd.evar_map ->
+  Vernacexpr.searchable -> Vernacexpr.search_restriction -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42259cee10..fe3bb9b890 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -40,6 +40,8 @@ let subprf = Entry.create "vernac:subprf"
 let quoted_attributes = Entry.create "vernac:quoted_attributes"
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
+let def_token = Entry.create "vernac:def_token"
+let assumption_token = Entry.create "vernac:assumption_token"
 let def_body = Entry.create "vernac:def_body"
 let decl_notations = Entry.create "vernac:decl_notations"
 let record_field = Entry.create "vernac:record_field"
@@ -70,6 +72,13 @@ let test_hash_ident =
   to_entry "test_hash_ident" begin
     lk_kw "#" >> lk_ident >> check_no_space
   end
+
+let test_id_colon =
+  let open Pcoq.Lookahead in
+  to_entry "test_id_colon" begin
+    lk_ident >> lk_kw ":"
+  end
+
 }
 
 GRAMMAR EXTEND Gram
@@ -183,7 +192,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
 
 (* Gallina declarations *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
+  GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion
     record_field decl_notations rec_definition ident_decl univ_decl;
 
   gallina:
@@ -915,7 +924,7 @@ GRAMMAR EXTEND Gram
           { fun g -> VernacSearch (SearchPattern c,g, l) }
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
           { fun g -> VernacSearch (SearchRewrite c,g, l) }
-      | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
+      | IDENT "Search"; s = search_query; l = search_queries; "." ->
           { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) }
       ] ]
   ;
@@ -1012,16 +1021,50 @@ GRAMMAR EXTEND Gram
   positive_search_mark:
     [ [ "-" -> { false } | -> { true } ] ]
   ;
-  searchabout_query:
-    [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter ->
-            { (b, SearchString (s,sc)) }
-      | b = positive_search_mark; p = constr_pattern ->
-            { (b, SearchSubPattern p) }
+  search_query:
+    [ [ b = positive_search_mark; s = search_item -> { (b, SearchLiteral s) }
+      | b = positive_search_mark; "["; l = LIST1 (LIST1 search_query) SEP "|"; "]" -> { (b, SearchDisjConj l) }
+      ] ]
+  ;
+  search_item:
+    [ [ test_id_colon; where = search_where; ":"; s = ne_string; sc = OPT scope_delimiter ->
+            { SearchString (where,s,sc) }
+      | IDENT "is"; ":"; kl = logical_kind ->
+            { SearchKind kl }
+      | s = ne_string; sc = OPT scope_delimiter ->
+            { SearchString ((Anywhere,false),s,sc) }
+      | test_id_colon; where = search_where; ":"; p = constr_pattern ->
+            { SearchSubPattern (where,p) }
+      | p = constr_pattern ->
+            { SearchSubPattern ((Anywhere,false),p) }
       ] ]
   ;
-  searchabout_queries:
+  logical_kind:
+    [ [ k = thm_token -> { IsProof k }
+      | k = assumption_token -> { IsAssumption (snd k) }
+      | k = IDENT "Context" -> { IsAssumption Context }
+      | k = extended_def_token -> { IsDefinition k }
+      | IDENT "Primitive" -> { IsPrimitive } ] ]
+  ;
+  extended_def_token:
+    [ [ k = def_token -> { snd k }
+      | IDENT "Coercion" -> { Coercion }
+      | IDENT "Instance" -> { Instance }
+      | IDENT "Scheme" -> { Scheme }
+      | IDENT "Canonical" -> { CanonicalStructure }
+      | IDENT "Field" -> { StructureComponent }
+      | IDENT "Method" -> { Method } ] ]
+  ;
+  search_where:
+    [ [ IDENT "head" -> { Anywhere, true }
+      | IDENT "hyp" -> { InHyp, false }
+      | IDENT "concl" -> { InConcl, false }
+      | IDENT "headhyp" -> { InHyp, true }
+      | IDENT "headconcl" -> { InConcl, true } ] ]
+  ;
+  search_queries:
     [ [ m = ne_in_or_out_modules -> { ([],m) }
-      | s = searchabout_query; l = searchabout_queries ->
+      | s = search_query; l = search_queries ->
         { let (sl,m) = l in (s::sl,m) }
       | -> { ([],SearchOutside []) }
       ] ]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b97cdfa51c..2c52c605b5 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -108,6 +108,38 @@ open Pputils
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
+  let string_of_theorem_kind = let open Decls in function
+    | Theorem -> "Theorem"
+    | Lemma -> "Lemma"
+    | Fact -> "Fact"
+    | Remark -> "Remark"
+    | Property -> "Property"
+    | Proposition -> "Proposition"
+    | Corollary -> "Corollary"
+
+  let string_of_definition_object_kind = let open Decls in function
+    | Definition -> "Definition"
+    | Example -> "Example"
+    | Coercion -> "Coercion"
+    | SubClass -> "SubClass"
+    | CanonicalStructure -> "Canonical Structure"
+    | Instance -> "Instance"
+    | Let -> "Let"
+    | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
+      CErrors.anomaly (Pp.str "Internal definition kind.")
+
+  let string_of_assumption_kind = let open Decls in function
+    | Definitional -> "Parameter"
+    | Logical -> "Axiom"
+    | Conjectural -> "Conjecture"
+    | Context -> "Context"
+
+  let string_of_logical_kind = let open Decls in function
+    | IsAssumption k -> string_of_assumption_kind k
+    | IsDefinition k -> string_of_definition_object_kind k
+    | IsProof k -> string_of_theorem_kind k
+    | IsPrimitive -> "Primitive"
+
   let pr_notation_entry = function
     | InConstrEntry -> keyword "constr"
     | InCustomEntry s -> keyword "custom" ++ spc () ++ str s
@@ -148,14 +180,28 @@ open Pputils
     | SearchOutside [] -> mt()
     | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l
 
-  let pr_search (b,c) =
-    (if b then str "-" else mt()) ++
-      match c with
-        | SearchSubPattern p ->
+  let pr_search_where = function
+    | Anywhere, false -> mt ()
+    | Anywhere, true -> str "head:"
+    | InHyp, true -> str "headhyp:"
+    | InHyp, false -> str "hyp:"
+    | InConcl, true -> str "headconcl:"
+    | InConcl, false -> str "concl:"
+
+  let pr_search_item = function
+        | SearchSubPattern (where,p) ->
           let env = Global.env () in
           let sigma = Evd.from_env env in
-          pr_constr_pattern_expr env sigma p
-        | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+          pr_search_where where ++ pr_constr_pattern_expr env sigma p
+        | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+        | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind)
+
+  let rec pr_search_request = function
+    | SearchLiteral a -> pr_search_item a
+    | SearchDisjConj l -> str "[" ++ prlist_with_sep spc (prlist_with_sep pr_bar pr_search_default) l ++ str "]"
+
+  and pr_search_default (b, s) =
+    (if b then mt() else str "-") ++ pr_search_request s
 
   let pr_search a gopt b pr_p =
     pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
@@ -165,7 +211,7 @@ open Pputils
       | 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 ->
-         keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b
+         keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_default sl ++ pr_in_out_modules b
 
   let pr_option_ref_value = function
     | Goptions.QualidRefValue id -> pr_qualid id
@@ -386,15 +432,6 @@ open Pputils
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
 
-let string_of_theorem_kind = let open Decls in function
-  | Theorem -> "Theorem"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Remark -> "Remark"
-  | Property -> "Property"
-  | Proposition -> "Proposition"
-  | Corollary -> "Corollary"
-
   let pr_thm_token k = keyword (string_of_theorem_kind k)
 
   let pr_syntax_modifier = let open Gramlib.Gramext in function
@@ -611,18 +648,6 @@ let string_of_theorem_kind = let open Decls in function
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
-
-let string_of_definition_object_kind = let open Decls in function
-  | Definition -> "Definition"
-  | Example -> "Example"
-  | Coercion -> "Coercion"
-  | SubClass -> "SubClass"
-  | CanonicalStructure -> "Canonical Structure"
-  | Instance -> "Instance"
-  | Let -> "Let"
-  | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    CErrors.anomaly (Pp.str "Internal definition kind.")
-
   let pr_vernac_expr v =
     let return = tag_vernac v in
     let env = Global.env () in
diff --git a/vernac/search.ml b/vernac/search.ml
index 8b54b696f2..2a21184c1e 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -17,11 +17,14 @@ open Libobject
 open Environ
 open Pattern
 open Libnames
+open Vernacexpr
 
 module NamedDecl = Context.Named.Declaration
 
-type filter_function = GlobRef.t -> env -> constr -> bool
-type display_function = GlobRef.t -> env -> constr -> unit
+type filter_function =
+  GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool
+type display_function =
+  GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
 
 (* This option restricts the output of [SearchPattern ...], etc.
 to the names of the symbols matching the
@@ -29,9 +32,15 @@ query, separated by a newline. This type of output is useful for
 editors (like emacs), to generate a list of completion candidates
 without having to parse through the types of all symbols. *)
 
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
+type glob_search_item =
+  | GlobSearchSubPattern of glob_search_where * bool * constr_pattern
   | GlobSearchString of string
+  | GlobSearchKind of Decls.logical_kind
+  | GlobSearchFilter of (GlobRef.t -> bool)
+
+type glob_search_request =
+  | GlobSearchLiteral of glob_search_item
+  | GlobSearchDisjConj of (bool * glob_search_request) list list
 
 module SearchBlacklist =
   Goptions.MakeStringTable
@@ -52,25 +61,9 @@ module SearchBlacklist =
 let iter_constructors indsp u fn env nconstr =
   for i = 1 to nconstr do
     let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
-    fn (GlobRef.ConstructRef (indsp, i)) env typ
+    fn (GlobRef.ConstructRef (indsp, i)) None env typ
   done
 
-let iter_named_context_name_type f =
-  List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
-
-let get_current_or_goal_context ?pstate glnum =
-  match pstate with
-  | None -> let env = Global.env () in Evd.(from_env env, env)
-  | Some p -> Declare.get_goal_context p glnum
-
-(* General search over hypothesis of a goal *)
-let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
-  let env = Global.env () in
-  let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in
-  let evmap,e = get_current_or_goal_context ?pstate glnum in
-  let pfctxt = named_context e in
-  iter_named_context_name_type iter_hyp pfctxt
-
 (* FIXME: this is a Libobject hack that should be replaced with a proper
    registration mechanism. *)
 module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end)
@@ -80,9 +73,8 @@ let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
 | exception Not_found -> ()
 
 (* General search over declarations *)
-let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
-  let env = Global.env () in
-  List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d))
+let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
+  List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d))
     (Environ.named_context env);
   let iter_obj (sp, kn) lobj = match lobj with
     | AtomicObject o ->
@@ -91,7 +83,8 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
           let cst = Global.constant_of_delta_kn kn in
           let gr = GlobRef.ConstRef cst in
           let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
-          fn gr env typ
+          let kind = Dumpglob.constant_kind cst in
+          fn gr (Some kind) env typ
         end @@
         DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
           let mind = Global.mind_of_delta_kn kn in
@@ -101,7 +94,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
             let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
             let i = (ind, u) in
             let typ = Inductiveops.type_of_inductive env i in
-            let () = fn (GlobRef.IndRef ind) env typ in
+            let () = fn (GlobRef.IndRef ind) None env typ in
             let len = Array.length mip.mind_user_lc in
             iter_constructors ind u fn env len
           in
@@ -115,12 +108,6 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()
 
-let generic_search ?pstate glnumopt fn =
-  (match glnumopt with
-  | None -> ()
-  | Some glnum -> iter_hypothesis ?pstate glnum fn);
-  iter_declarations fn
-
 (** This module defines a preference on constrs in the form of a
     [compare] function (preferred constr must be big for this
     functions, so preferences such as small constr must use a reversed
@@ -132,7 +119,7 @@ module ConstrPriority = struct
 
   (* The priority is memoised here. Because of the very localised use
      of this module, it is not worth it making a convenient interface. *)
-  type t = GlobRef.t * Environ.env * Constr.t * priority
+  type t = GlobRef.t * Decls.logical_kind option * Environ.env * Constr.t * priority
   and priority = int
 
   module ConstrSet = CSet.Make(Constr)
@@ -154,10 +141,10 @@ module ConstrPriority = struct
   let num_symbols t =
     ConstrSet.(cardinal (symbols empty t))
 
-  let priority t : priority =
+  let priority gref t : priority =
     -(3*(num_symbols t) + size t)
 
-  let compare (_,_,_,p1) (_,_,_,p2) =
+  let compare (_,_,_,_,p1) (_,_,_,_,p2) =
     pervasives_compare p1 p2
 end
 
@@ -172,16 +159,16 @@ let rec iter_priority_queue q fn =
       with Heap.EmptyHeap -> None
   end in
   match next with
-  | Some (gref,env,t,_) ->
-    fn gref env t;
+  | Some (gref,kind,env,t,_) ->
+    fn gref kind env t;
     iter_priority_queue (PriorityQueue.remove q) fn
   | None -> ()
 
 let prioritize_search seq fn =
   let acc = ref PriorityQueue.empty in
-  let iter gref env t =
-    let p = ConstrPriority.priority t in
-    acc := PriorityQueue.add (gref,env,t,p) !acc
+  let iter gref kind env t =
+    let p = ConstrPriority.priority gref t in
+    acc := PriorityQueue.add (gref,kind,env,t,p) !acc
   in
   let () = seq iter in
   iter_priority_queue !acc fn
@@ -211,12 +198,12 @@ let full_name_of_reference ref =
   DirPath.to_string dir ^ "." ^ Id.to_string id
 
 (** Whether a reference is blacklisted *)
-let blacklist_filter ref env typ =
+let blacklist_filter ref kind env sigma typ =
   let name = full_name_of_reference ref in
   let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
   CString.Set.for_all is_not_bl (SearchBlacklist.v ())
 
-let module_filter (mods, outside) ref env typ =
+let module_filter (mods, outside) ref kind env sigma typ =
   let sp = Nametab.path_of_global ref in
   let sl = dirpath sp in
   let is_outside md = not (is_dirpath_prefix_of md sl) in
@@ -226,25 +213,42 @@ let module_filter (mods, outside) ref env typ =
 
 let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
 
-let search_filter query gr env typ = match query with
-| GlobSearchSubPattern pat ->
-  Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ)
+let search_filter query gr kind env sigma typ = match query with
+| GlobSearchSubPattern (where,head,pat) ->
+  let open Context.Rel.Declaration in
+  let collect_hyps ctx =
+    List.fold_left (fun acc d -> match get_value d with
+                       | None -> get_type d :: acc
+                       | Some b -> b :: get_type d :: acc) [] ctx in
+  let typl= match where with
+  | InHyp -> collect_hyps (fst (Term.decompose_prod_assum typ))
+  | InConcl -> [snd (Term.decompose_prod_assum typ)]
+  | Anywhere ->
+      if head then
+        let ctx, ccl = Term.decompose_prod_assum typ in ccl :: collect_hyps ctx
+      else [typ] in
+  List.exists (fun typ ->
+      let f =
+        if head then Constr_matching.is_matching_head
+        else Constr_matching.is_matching_appsubterm ~closed:false in
+      f env sigma pat (EConstr.of_constr typ)) typl
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
-
+| GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k')
+| GlobSearchFilter f -> f gr
 
 (** SearchPattern *)
 
-let search_pattern ?pstate gopt pat mods pr_search =
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+let search_pattern env sigma pat mods pr_search =
+  let filter ref kind env typ =
+    module_filter mods ref kind env sigma typ &&
+    pattern_filter pat ref env sigma (EConstr.of_constr typ) &&
+    blacklist_filter ref kind env sigma typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** SearchRewrite *)
 
@@ -256,47 +260,49 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
 
-let search_rewrite ?pstate gopt pat mods pr_search =
+let search_rewrite env sigma pat mods pr_search =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) ||
-       pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) &&
-    blacklist_filter ref env typ
+  let filter ref kind env typ =
+    module_filter mods ref kind env sigma typ &&
+    (pattern_filter pat1 ref env sigma (EConstr.of_constr typ) ||
+       pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) &&
+    blacklist_filter ref kind env sigma typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** Search *)
 
-let search_by_head ?pstate gopt pat mods pr_search =
-  let filter ref env typ =
-    module_filter mods ref env typ &&
-    head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+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 env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 (** Search *)
 
-let search ?pstate gopt items mods pr_search =
-  let filter ref env typ =
+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
-    module_filter mods ref env typ &&
-    List.for_all
-      (fun (b,i) -> eqb b (search_filter i ref env typ)) items &&
-    blacklist_filter ref env typ
+    module_filter mods ref kind env sigma typ &&
+      let rec aux = function
+        | GlobSearchLiteral i -> search_filter i ref kind env sigma typ
+        | GlobSearchDisjConj l -> List.exists (List.for_all aux') l
+      and aux' (b,s) = eqb b (aux s) in
+      List.for_all aux' items && blacklist_filter ref kind env sigma typ
   in
-  let iter ref env typ =
-    if filter ref env typ then pr_search ref env typ
+  let iter ref kind env typ =
+    if filter ref kind env typ then pr_search ref kind env typ
   in
-  generic_search ?pstate gopt iter
+  generic_search env iter
 
 type search_constraint =
   | Name_Pattern of Str.regexp
@@ -311,7 +317,7 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-let interface_search ?pstate =
+let interface_search env sigma =
   let rec extract_flags name tpe subtpe mods blacklist = function
   | [] -> (name, tpe, subtpe, mods, blacklist)
   | (Name_Pattern regexp, b) :: l ->
@@ -325,7 +331,7 @@ let interface_search ?pstate =
   | (Include_Blacklist, b) :: l ->
     extract_flags name tpe subtpe mods b l
   in
-  fun ?glnum flags ->
+  fun flags ->
   let (name, tpe, subtpe, mods, blacklist) =
     extract_flags [] [] [] [] false flags
   in
@@ -337,12 +343,12 @@ let interface_search ?pstate =
       toggle (Str.string_match regexp id 0) flag
     in
     let match_type (pat, flag) =
-      toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
+      toggle (Constr_matching.is_matching env sigma pat (EConstr.of_constr constr)) flag
     in
     let match_subtype (pat, flag) =
       toggle
         (Constr_matching.is_matching_appsubterm ~closed:false
-           env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
+           env sigma pat (EConstr.of_constr constr)) flag
     in
     let match_module (mdl, flag) =
       toggle (Libnames.is_dirpath_prefix_of mdl path) flag
@@ -351,7 +357,7 @@ let interface_search ?pstate =
     List.for_all match_type tpe &&
     List.for_all match_subtype subtpe &&
     List.for_all match_module mods &&
-    (blacklist || blacklist_filter ref env constr)
+    (blacklist || blacklist_filter ref kind env sigma constr)
   in
   let ans = ref [] in
   let print_function ref env constr =
@@ -377,8 +383,8 @@ let interface_search ?pstate =
     } in
     ans := answer :: !ans;
   in
-  let iter ref env typ =
+  let iter ref kind env typ =
     if filter_function ref env typ then print_function ref env typ
   in
-  let () = generic_search ?pstate glnum iter in
+  let () = generic_search env iter in
   !ans
diff --git a/vernac/search.mli b/vernac/search.mli
index d3b8444b5f..09847f4e03 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -12,15 +12,24 @@ open Names
 open Constr
 open Environ
 open Pattern
+open Vernacexpr
 
 (** {6 Search facilities. } *)
 
-type glob_search_about_item =
-  | GlobSearchSubPattern of constr_pattern
+type glob_search_item =
+  | GlobSearchSubPattern of glob_search_where * bool * constr_pattern
   | GlobSearchString of string
+  | GlobSearchKind of Decls.logical_kind
+  | GlobSearchFilter of (GlobRef.t -> bool)
 
-type filter_function = GlobRef.t -> env -> constr -> bool
-type display_function = GlobRef.t -> env -> constr -> unit
+type glob_search_request =
+  | GlobSearchLiteral of glob_search_item
+  | GlobSearchDisjConj of (bool * glob_search_request) list list
+
+type filter_function =
+  GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool
+type display_function =
+  GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
 
 (** {6 Generic filter functions} *)
 
@@ -30,7 +39,7 @@ val blacklist_filter : filter_function
 val module_filter : DirPath.t list * bool -> filter_function
 (** Check whether a reference pertains or not to a set of modules *)
 
-val search_filter : glob_search_about_item -> filter_function
+val search_filter : glob_search_item -> filter_function
 
 (** {6 Specialized search functions}
 
@@ -38,13 +47,13 @@ val search_filter : glob_search_about_item -> filter_function
 goal and the global environment for things matching [pattern] and
 satisfying module exclude/include clauses of [modinout]. *)
 
-val search_by_head : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
+val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_about_item) list
+val search         : env -> Evd.evar_map -> (bool * glob_search_request) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
@@ -65,12 +74,11 @@ type 'a coq_object = {
   coq_object_object : 'a;
 }
 
-val interface_search : ?pstate:Declare.Proof.t -> ?glnum:int -> (search_constraint * bool) list ->
-  constr coq_object list
+val interface_search : env -> Evd.evar_map -> (search_constraint * bool) list -> constr coq_object list
 
 (** {6 Generic search function} *)
 
-val generic_search : ?pstate:Declare.Proof.t -> int option -> display_function -> unit
+val generic_search : env -> display_function -> unit
 (** This function iterates over all hypothesis of the goal numbered
     [glnum] (if present) and all known declarations. *)
 
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 618a61f487..a09a473afe 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -32,6 +32,7 @@ ComPrimitive
 ComAssumption
 DeclareInd
 Search
+ComSearch
 Prettyp
 ComInductive
 ComFixpoint
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 09201d727d..35e625859b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1762,91 +1762,17 @@ let vernac_print ~pstate ~atts =
   | PrintStrategy r -> print_strategy r
   | PrintRegistered -> print_registered ()
 
-let global_module qid =
-  try Nametab.full_name_module qid
-  with Not_found ->
-    user_err ?loc:qid.CAst.loc ~hdr:"global_module"
-     (str "Module/section " ++ pr_qualid qid ++ str " not found.")
-
-let interp_search_restriction = function
-  | SearchOutside l -> (List.map global_module l, true)
-  | SearchInside l -> (List.map global_module l, false)
-
-open Search
-
-let interp_search_about_item env sigma =
-  function
-  | SearchSubPattern pat ->
-      let _,pat = Constrintern.intern_constr_pattern env sigma pat in
-      GlobSearchSubPattern pat
-  | SearchString (s,None) when Id.is_valid s ->
-      GlobSearchString s
-  | SearchString (s,sc) ->
-      try
-        let ref =
-          Notation.interp_notation_as_global_reference
-            ~head:false (fun _ -> true) s sc in
-        GlobSearchSubPattern (Pattern.PRef ref)
-      with UserError _ ->
-        user_err ~hdr:"interp_search_about_item"
-          (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
-
-(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the
-   `search_output_name_only` option to avoid excessive printing when
-   searching.
-
-   The motivation was to make search usable for IDE completion,
-   however, it is still too slow due to the non-indexed nature of the
-   underlying search mechanism.
-
-   In the future we should deprecate the option and provide a fast,
-   indexed name-searching interface.
-*)
-let search_output_name_only = ref false
-
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Search";"Output";"Name";"Only"];
-      optread  = (fun () -> !search_output_name_only);
-      optwrite = (:=) search_output_name_only }
-
 let vernac_search ~pstate ~atts s gopt r =
+  let open ComSearch in
   let gopt = query_command_selector gopt in
-  let r = interp_search_restriction r in
-  let env,gopt =
+  let sigma, env =
     match gopt with | None ->
       (* 1st goal by default if it exists, otherwise no goal at all *)
-      (try snd (get_goal_or_global_context ~pstate 1) , Some 1
-       with _ -> Global.env (),None)
+      (try get_goal_or_global_context ~pstate 1
+       with _ -> let env = Global.env () in (Evd.from_env env, env))
     (* if goal selector is given and wrong, then let exceptions be raised. *)
-    | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
-  in
-  let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in
-  let pr_search ref env c =
-    let pr = pr_global ref in
-    let pp = if !search_output_name_only
-      then pr
-      else begin
-        let open Impargs in
-        let impargs = select_stronger_impargs (implicits_of_global ref) in
-        let impargs = List.map binding_kind_of_status impargs in
-        let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in
-        hov 2 (pr ++ str":" ++ spc () ++ pc)
-      end
-    in Feedback.msg_notice pp
-  in
-  (match s with
-  | SearchPattern c ->
-      (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
-  | SearchRewrite c ->
-      (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
-  | SearchHead c ->
-      (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
-  | Search sl ->
-      (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
-       Search.prioritize_search) pr_search);
-  Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
+    | Some g -> get_goal_or_global_context ~pstate g in
+  interp_search env sigma s r
 
 let vernac_locate ~pstate = let open Constrexpr in function
   | LocateAny {v=AN qid}  -> Prettyp.print_located_qualid qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b622fd9801..0fdf9e2a7b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -61,15 +61,22 @@ type printable =
   | PrintStrategy of qualid or_by_notation option
   | PrintRegistered
 
-type search_about_item =
-  | SearchSubPattern of constr_pattern_expr
-  | SearchString of string * scope_name option
+type glob_search_where = InHyp | InConcl | Anywhere
+
+type search_item =
+  | SearchSubPattern of (glob_search_where * bool) * constr_pattern_expr
+  | SearchString of (glob_search_where * bool) * string * scope_name option
+  | SearchKind of Decls.logical_kind
+
+type search_request =
+  | SearchLiteral of search_item
+  | SearchDisjConj of (bool * search_request) list list
 
 type searchable =
   | SearchPattern of constr_pattern_expr
   | SearchRewrite of constr_pattern_expr
   | SearchHead of constr_pattern_expr
-  | Search of (bool * search_about_item) list
+  | Search of (bool * search_request) list
 
 type locatable =
   | LocateAny of qualid or_by_notation
author	Emilio Jesus Gallego Arias	2020-05-16 19:21:05 +0200
committer	Emilio Jesus Gallego Arias	2020-05-16 19:21:05 +0200
commit	2b0df4db404a1eb5b149e87ae0d23a5352b18f67 (patch)
tree	0c127222b11fb7b8a32e1d9835cdc888b024364e
parent	05e811a81de90ce698c4f0317d549dc01dc13e17 (diff)
parent	ca0002823429a6c7de953446b6d351332d24daa7 (diff)