Evarsolve (coq-core.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

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.

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:

ev does not occur in c.
c does not contain any Meta(_)

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

val instantiate_evar : 
  unifier ->
  unify_flags ->
  Environ.env ->
  Evd.evar_map ->
  Evar.t ->
  EConstr.constr ->
  Evd.evar_map

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