Search: new clauses for searching head, conclusion, kind...

- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict
  match to an hypothesis or the conclusion, possibly only at the head
  (like SearchHead in this latter case)
- new clause "is:" to search by kind of object (for some list of kinds)
- support for any combination of negations, disjunctions and conjunctions,
  using a syntax close to that of intropatterns.

10 files changed, 260 insertions, 112 deletions

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..bc6f054d09 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -310,7 +310,7 @@ let interp_search_notation ?loc tag okey =
   | 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
+  Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
 
 }
 
@@ -401,9 +401,9 @@ 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
+  fun gr kind env typ ->
+    let ans = Search.search_filter arg gr kind 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
@@ -413,18 +413,20 @@ let interp_search_arg arg =
   | RGlobSearchSubPattern p ->
     let env = Global.env () in
     let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in
-    Search.GlobSearchSubPattern p) arg
+    Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,p)) arg
   in
   let hpat, a1 = match arg with
-  | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a'
-  | (true, Search.GlobSearchSubPattern p) :: a' ->
+  | (_, 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 env typ -> hpat typ)
+  interp_search_about (a2 @ a3) (fun gr kind env typ -> hpat typ)
 
 (* Module path postfilter *)
 
@@ -455,10 +457,10 @@ let interp_modloc mr =
     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
+  | [] -> 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
+  fun gr kind env typ -> is_in gr kind env typ && is_out gr kind env typ
 
 (* The unified, extended vernacular "Search" command *)
 
@@ -472,9 +474,9 @@ 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
+    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
     Search.generic_search None display }
 END
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/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 92f6d140d5..181c75702d 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 -> 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
@@ -30,8 +33,14 @@ editors (like emacs), to generate a list of completion candidates
 without having to parse through the types of all symbols. *)
 
 type glob_search_item =
-  | GlobSearchSubPattern of constr_pattern
+  | 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,7 +61,7 @@ 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 =
@@ -64,9 +73,9 @@ let get_current_or_goal_context ?pstate glnum =
   | 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 iter_hypothesis ?pstate glnum (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
   let env = Global.env () in
-  let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in
+  let iter_hyp idh typ = fn (GlobRef.VarRef idh) None 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
@@ -80,9 +89,9 @@ 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 iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
   let env = Global.env () in
-  List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d))
+  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 +100,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 +111,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
@@ -132,7 +142,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)
@@ -157,7 +167,7 @@ module ConstrPriority = struct
   let priority t : priority =
     -(3*(num_symbols t) + size t)
 
-  let compare (_,_,_,p1) (_,_,_,p2) =
+  let compare (_,_,_,_,p1) (_,_,_,_,p2) =
     pervasives_compare p1 p2
 end
 
@@ -172,16 +182,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 iter gref kind env t =
     let p = ConstrPriority.priority t in
-    acc := PriorityQueue.add (gref,env,t,p) !acc
+    acc := PriorityQueue.add (gref,kind,env,t,p) !acc
   in
   let () = seq iter in
   iter_priority_queue !acc fn
@@ -211,12 +221,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 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 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,23 +236,40 @@ 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 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 (Evd.from_env env) 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 &&
+  let filter ref kind env typ =
+    module_filter mods ref kind env typ &&
     pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+    blacklist_filter ref kind env 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
 
@@ -259,42 +286,44 @@ let rewrite_pat2 pat =
 let search_rewrite ?pstate gopt 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 &&
+  let filter ref kind env typ =
+    module_filter mods ref kind 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
+    blacklist_filter ref kind env 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
 
 (** Search *)
 
 let search_by_head ?pstate gopt pat mods pr_search =
-  let filter ref env typ =
-    module_filter mods ref env typ &&
+  let filter ref kind env typ =
+    module_filter mods ref kind env typ &&
     head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
-    blacklist_filter ref env typ
+    blacklist_filter ref kind env 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
 
 (** Search *)
 
 let search ?pstate gopt items mods pr_search =
-  let filter ref env typ =
+  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 typ &&
+      let rec aux = function
+        | GlobSearchLiteral i -> search_filter i ref kind env 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 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
 
@@ -351,7 +380,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 constr)
   in
   let ans = ref [] in
   let print_function ref env constr =
@@ -377,7 +406,7 @@ 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
diff --git a/vernac/search.mli b/vernac/search.mli
index 5eeb77a6d0..3dc437d85a 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_item =
-  | GlobSearchSubPattern of constr_pattern
+  | 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 -> constr -> bool
+type display_function =
+  GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
 
 (** {6 Generic filter functions} *)
 
@@ -44,7 +53,7 @@ val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern ->
                   -> display_function -> unit
 val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool
                   -> display_function -> unit
-val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_item) list
+val search         : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_request) list
                   -> DirPath.t list * bool -> display_function -> unit
 
 type search_constraint =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 62d97fb845..80bd1ac727 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1774,22 +1774,51 @@ let interp_search_restriction = function
 
 open Search
 
+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 pat ->
+  | SearchSubPattern ((where,head),pat) ->
       let _,pat = Constrintern.intern_constr_pattern env sigma pat in
-      GlobSearchSubPattern pat
-  | SearchString (s,None) when Id.is_valid s ->
+      GlobSearchSubPattern (where,head,pat)
+  | SearchString ((Anywhere,false),s,None) when Id.is_valid s ->
       GlobSearchString s
-  | SearchString (s,sc) ->
-      try
+  | SearchString ((where,head),s,sc) ->
+      (try
         let ref =
           Notation.interp_notation_as_global_reference
             ~head:false (fun _ -> true) s sc in
-        GlobSearchSubPattern (Pattern.PRef ref)
+        GlobSearchSubPattern (where,head,Pattern.PRef ref)
       with UserError _ ->
         user_err ~hdr:"interp_search_item"
-          (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
+          (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component"))
+  | 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
@@ -1823,7 +1852,7 @@ let vernac_search ~pstate ~atts s gopt r =
     | 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_search ref kind env c =
     let pr = pr_global ref in
     let pp = if !search_output_name_only
       then pr
@@ -1844,7 +1873,7 @@ let vernac_search ~pstate ~atts s gopt r =
   | 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_item env Evd.(from_env env))) sl) r |>
+      (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |>
        Search.prioritize_search) pr_search);
   Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c3ae1993cd..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 glob_search_where = InHyp | InConcl | Anywhere
+
 type search_item =
-  | SearchSubPattern of constr_pattern_expr
-  | SearchString of string * scope_name option
+  | 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_item) list
+  | Search of (bool * search_request) list
 
 type locatable =
   | LocateAny of qualid or_by_notation