package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.

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