package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type alias
val of_alias : alias -> EConstr.t
module AllowedEvars : sig ... end
type unify_flags = {
  1. modulo_betaiota : bool;
  2. open_ts : TransparentState.t;
  3. closed_ts : TransparentState.t;
  4. subterm_ts : TransparentState.t;
  5. allowed_evars : AllowedEvars.t;
  6. allow_K_at_toplevel : bool;
  7. with_cs : bool;
}
type unification_result =
  1. | Success of Evd.evar_map
  2. | UnifFailure of Evd.evar_map * Pretype_errors.unification_error
val is_success : unification_result -> bool
val is_evar_allowed : unify_flags -> Evar.t -> bool
val expand_vars_in_term : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type unification_kind =
  1. | TypeUnification
  2. | TermUnification
val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map
val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool -> ?refreshset:bool -> bool option -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> Evar.t -> EConstr.constr list -> EConstr.constr list -> Evd.evar_map
val solve_evar_evar : ?force:bool -> (Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map) -> unifier -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.existential -> Evd.evar_map
val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> (bool option * EConstr.existential * EConstr.constr) -> unification_result
val reconsider_unif_constraints : unifier -> unify_flags -> Evd.evar_map -> unification_result
val is_unification_pattern_evar : Environ.env -> Evd.evar_map -> EConstr.existential -> EConstr.constr list -> EConstr.constr -> alias list option
val is_unification_pattern : (Environ.env * int) -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr -> alias list option
val solve_pattern_eqn : Environ.env -> Evd.evar_map -> alias list -> EConstr.constr -> EConstr.constr
val noccur_evar : Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> bool
exception IllTypedInstance of Environ.env * EConstr.types * EConstr.types
val check_evar_instance : unifier -> unify_flags -> Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> Evd.evar_map
val remove_instance_local_defs : Evd.evar_map -> Evar.t -> 'a list -> 'a list
val get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types