Merge PR #8855: More search options

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

9 files changed, 390 insertions, 220 deletions

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