package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cpattern
val pr_cpattern : cpattern -> Pp.t
type rpattern
val pr_rpattern : rpattern -> Pp.t
exception NoMatch
exception NoProgress
type (!'ident, !'term) ssrpattern =
  1. | T of 'term
  2. | In_T of 'term
  3. | X_In_T of 'ident * 'term
  4. | In_X_In_T of 'ident * 'term
  5. | E_In_X_In_T of 'term * 'ident * 'term
  6. | E_As_X_In_T of 'term * 'ident * 'term
val pp_pattern : Environ.env -> pattern -> Pp.t
val redex_of_pattern : ?resolve_typeclasses:bool -> Environ.env -> pattern -> Constr.constr Evd.in_evar_universe_context
val interp_rpattern : Goal.goal Evd.sigma -> rpattern -> pattern
type occ = (bool * int list) option
val eval_pattern : ?raise_NoMatch:bool -> Environ.env -> Evd.evar_map -> Constr.constr -> pattern option -> occ -> subst -> Constr.constr
val fill_occ_pattern : ?raise_NoMatch:bool -> Environ.env -> Evd.evar_map -> Constr.constr -> pattern -> occ -> int -> Constr.constr Evd.in_evar_universe_context * Constr.constr
type ssrdir =
  1. | L2R
  2. | R2L
val pr_dir_side : ssrdir -> Pp.t
type tpattern
type find_P = Environ.env -> Constr.constr -> int -> k:subst -> Constr.constr
type conclude = unit -> Constr.constr * ssrdir * (Evd.evar_map * UState.t * Constr.constr)
val mk_tpattern_matcher : ?all_instances:bool -> ?raise_NoMatch:bool -> ?upats_origin:(ssrdir * Constr.constr) -> Evd.evar_map -> occ -> (Evd.evar_map * tpattern list) -> find_P * conclude
val pf_fill_occ_term : Goal.goal Evd.sigma -> occ -> (Evd.evar_map * EConstr.t) -> EConstr.t * EConstr.t
val cpattern_of_term : (char * Genintern.glob_constr_and_expr) -> Geninterp.interp_sign -> cpattern
val do_once : 'a option ref -> (unit -> 'a) -> unit
val assert_done : 'a option ref -> 'a
val tag_of_cpattern : cpattern -> char
val loc_of_cpattern : cpattern -> Loc.t option
val id_of_pattern : pattern -> Names.Id.t option
val is_wildcard : cpattern -> bool
val cpattern_of_id : Names.Id.t -> cpattern
val pr_constr_pat : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_econstr_pat : Environ.env -> Evd.evar_map -> Evd.econstr -> Pp.t
val pf_unsafe_merge_uc : UState.t -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
val debug : bool -> unit
val ssrinstancesof : cpattern -> Tacmach.tactic
module Internal : sig ... end
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