package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.vernac/Search/index.html
Module SearchSource
Search facilities.
type glob_search_item = | GlobSearchSubPattern of Vernacexpr.glob_search_where * bool * Pattern.constr_pattern| GlobSearchString of string| GlobSearchKind of Decls.logical_kind| GlobSearchFilter of Names.GlobRef.t -> bool
type glob_search_request = | GlobSearchLiteral of glob_search_item| GlobSearchDisjConj of (bool * glob_search_request) list list
type filter_function =
Names.GlobRef.t ->
Decls.logical_kind option ->
Environ.env ->
Evd.evar_map ->
Constr.constr ->
booltype display_function =
Names.GlobRef.t ->
Decls.logical_kind option ->
Environ.env ->
Constr.constr ->
unitGeneric filter functions
Check whether a reference is blacklisted.
Check whether a reference pertains or not to a set of modules
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_rewrite :
Environ.env ->
Evd.evar_map ->
Pattern.constr_pattern ->
(Names.DirPath.t list * bool) ->
display_function ->
unitval search_pattern :
Environ.env ->
Evd.evar_map ->
Pattern.constr_pattern ->
(Names.DirPath.t list * bool) ->
display_function ->
unitval search :
Environ.env ->
Evd.evar_map ->
(bool * glob_search_request) list ->
(Names.DirPath.t list * bool) ->
display_function ->
unittype 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
*)
val interface_search :
Environ.env ->
Evd.evar_map ->
(search_constraint * bool) list ->
Constr.constr coq_object listGeneric 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.