package coq

  1. Overview
  2. Docs
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 : Environ.env -> Evd.evar_map -> 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 -> unit Proofview.tactic
module Internal : sig ... end
OCaml

Innovation. Community. Security.