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;
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

One might want to use different conversion strategies for types and terms: e.g. preventing delta reductions when doing term unifications but allowing arbitrary delta conversion when checking the types of evar instances.

type unification_kind =
| TypeUnification
| TermUnification

A unification function parameterized by:

  • unification flags
  • the kind of unification
  • environment
  • sigma
  • conversion problem
  • the two terms to unify.

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.

instantiate_evar unify flags env sigma ev c defines the evar ev with c, checking that the type of c is unifiable with ev's declared type first.

Preconditions:

If ev and c have non inferably convertible types, an exception IllTypedInstance is raised

evar_define choose env ev c try to instantiate ev with c (typed in env), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given ev; If ev and c have non inferably convertible types, an exception IllTypedInstance is raised

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 SList.t -> EConstr.constr SList.t -> 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 * Evd.evar_map * 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 : ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types