Module Search

Search facilities.
type glob_search_about_item =
| GlobSearchSubPattern of Pattern.constr_pattern
| GlobSearchString of string
type filter_function = Names.GlobRef.t -> Environ.env -> Constr.constr -> bool
type display_function = Names.GlobRef.t -> Environ.env -> Constr.constr -> unit
Generic filter functions
val blacklist_filter : filter_function

Check whether a reference is blacklisted.

val module_filter : (Names.DirPath.t list * bool) -> filter_function

Check whether a reference pertains or not to a set of modules

val search_about_filter : glob_search_about_item -> filter_function

Check whether a reference matches a SearchAbout query.

Specialized search functions

search_xxx gl pattern modinout searches the hypothesis of the glth goal and the global environment for things matching pattern and satisfying module exclude/include clauses of modinout.

val search_by_head : ?⁠pstate:Proof_global.t -> int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_rewrite : ?⁠pstate:Proof_global.t -> int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_pattern : ?⁠pstate:Proof_global.t -> int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_about : ?⁠pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list -> (Names.DirPath.t list * bool) -> display_function -> unit
type search_constraint =
| Name_Pattern of Str.regexp

Whether the name satisfies a regexp (uses Ocaml Str syntax)

| Type_Pattern of Pattern.constr_pattern

Whether the object type satisfies a pattern

| SubType_Pattern of Pattern.constr_pattern

Whether some subtype of object type satisfies a pattern

| In_Module of Names.DirPath.t

Whether the object pertains to a module

| Include_Blacklist

Bypass the Search blacklist

type 'a coq_object = {
coq_object_prefix : string list;
coq_object_qualid : string list;
coq_object_object : 'a;
}
Generic search function

This function iterates over all hypothesis of the goal numbered glnum (if present) and all known declarations.

Search function modifiers

prioritize_search iter iterates over the values of iter (seen as a sequence of declarations), in a relevance order. This requires to perform the entire iteration of iter before starting streaming. So prioritize_search should not be used for low-latency streaming.