Module Evarsolve

type alias
val of_alias : alias -> EConstr.t
module AllowedEvars : sig ... end
type unify_flags = {
modulo_betaiota : bool;
open_ts : TransparentState.t;
closed_ts : TransparentState.t;
subterm_ts : TransparentState.t;
allowed_evars : AllowedEvars.t;
allow_K_at_toplevel : bool;
with_cs : bool;
}
type unification_result =
| Success of Evd.evar_map
| 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

Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context

type unification_kind =
| TypeUnification
| TermUnification
type unifier = unify_flags -> unification_kind -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> unification_result

A unification function parameterized by:

  • unification flags
  • the kind of unification
  • environment
  • sigma
  • conversion problem
  • the two terms to unify.
type conversion_check = unify_flags -> unification_kind -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> bool

A conversion function: parameterized by the kind of unification, environment, sigma, conversion problem and the two terms to convert. Conversion is not allowed to instantiate evars contrary to unification.

val instantiate_evar : unifier -> unify_flags -> Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> Evd.evar_map
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

The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised

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

May raise IllTypedInstance if types are not convertible

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