package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type core_unify_flags = {
  1. modulo_conv_on_closed_terms : TransparentState.t option;
  2. use_metas_eagerly_in_conv_on_closed_terms : bool;
  3. use_evars_eagerly_in_conv_on_closed_terms : bool;
  4. modulo_delta : TransparentState.t;
  5. modulo_delta_types : TransparentState.t;
  6. check_applied_meta_types : bool;
  7. use_pattern_unification : bool;
  8. use_meta_bound_pattern_unification : bool;
  9. allowed_evars : Evarsolve.AllowedEvars.t;
  10. restrict_conv_on_strict_subterms : bool;
  11. modulo_betaiota : bool;
  12. modulo_eta : bool;
}
type unify_flags = {
  1. core_unify_flags : core_unify_flags;
  2. merge_unify_flags : core_unify_flags;
  3. subterm_unify_flags : core_unify_flags;
  4. allow_K_in_toplevel_higher_order_unification : bool;
  5. resolve_evars : bool;
}
val default_core_unify_flags : unit -> core_unify_flags
val default_no_delta_core_unify_flags : unit -> core_unify_flags
val default_unify_flags : unit -> unify_flags
val default_no_delta_unify_flags : TransparentState.t -> unify_flags
val elim_flags : unit -> unify_flags
val elim_no_delta_flags : unit -> unify_flags
val is_keyed_unification : unit -> bool
val w_unify_to_subterm_all : Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Evd.evar_map * EConstr.constr) list
val w_unify_meta_types : Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Evd.evar_map
exception PatternNotFound
type prefix_of_inductive_support_flag = bool
type abstraction_request =
  1. | AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map * EConstr.constr * Locus.clause * bool
  2. | AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool
val pose_all_metas_as_evars : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
type subst0 = Evd.evar_map * metabinding list * ((Environ.env * int) * EConstr.existential * EConstr.t) list
val w_merge : Environ.env -> bool -> core_unify_flags -> subst0 -> Evd.evar_map
val unify_0_with_initial_metas : subst0 -> bool -> Environ.env -> Evd.conv_pb -> core_unify_flags -> EConstr.types -> EConstr.types -> subst0