package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Search facilities.
type 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
type glob_search_request =
  1. | GlobSearchLiteral of glob_search_item
  2. | 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 -> bool
type display_function = Names.GlobRef.t -> Decls.logical_kind option -> 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_filter : glob_search_item -> filter_function
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 -> unit
val search_pattern : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
type 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

    *)
type '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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct