package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.vernac/Search/index.html

Module SearchSource

Search facilities.
Sourcetype glob_search_item =
  1. | GlobSearchSubPattern of Vernacexpr.glob_search_where * bool * Pattern.constr_pattern
  2. | GlobSearchString of string
  3. | GlobSearchKind of Decls.logical_kind
  4. | GlobSearchFilter of Names.GlobRef.t -> bool
Sourcetype glob_search_request =
  1. | GlobSearchLiteral of glob_search_item
  2. | GlobSearchDisjConj of (bool * glob_search_request) list list
Sourcetype filter_function = Names.GlobRef.t -> Decls.logical_kind option -> Environ.env -> Evd.evar_map -> Constr.constr -> bool
Sourcetype display_function = Names.GlobRef.t -> Decls.logical_kind option -> Environ.env -> Constr.constr -> unit
Generic filter functions
Sourceval blacklist_filter : filter_function

Check whether a reference is blacklisted.

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

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.

Sourceval search_rewrite : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
Sourceval search_pattern : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
Sourcetype search_constraint =
  1. | Name_Pattern of Str.regexp
    (*

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

    *)
  2. | Type_Pattern of Pattern.constr_pattern
    (*

    Whether the object type satisfies a pattern

    *)
  3. | SubType_Pattern of Pattern.constr_pattern
    (*

    Whether some subtype of object type satisfies a pattern

    *)
  4. | In_Module of Names.DirPath.t
    (*

    Whether the object pertains to a module

    *)
  5. | Include_Blacklist
    (*

    Bypass the Search blacklist

    *)
Sourcetype 'a coq_object = {
  1. coq_object_prefix : string list;
  2. coq_object_qualid : string list;
  3. 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.