Module `Evarsolve`Source

Sourcetype alias

Sourceval of_alias : alias -> EConstr.t

Sourcemodule AllowedEvars : sig ... end

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

}

Sourcetype unification_result =

| Success of Evd.evar_map
| UnifFailure of Evd.evar_map * Pretype_errors.unification_error

Sourceval is_success : unification_result -> bool

Sourceval is_evar_allowed : unify_flags -> Evar.t -> bool

Source

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.

Sourcetype unification_kind =

| TypeUnification
| TermUnification

Source

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.

Source

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

Source

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

Source

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

Source

val refresh_universes : 
  ?status:Evd.rigid ->
  ?onlyalg:bool ->
  ?refreshset:bool ->
  bool option ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Evd.evar_map * EConstr.types

Source

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

Source

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

Source

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

Source

val reconsider_unif_constraints : 
  unifier ->
  unify_flags ->
  Evd.evar_map ->
  unification_result

Source

val is_unification_pattern_evar : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.existential ->
  EConstr.constr list ->
  EConstr.constr ->
  alias list option

Source

val is_unification_pattern : 
  (Environ.env * int) ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr ->
  alias list option

Source

val solve_pattern_eqn : 
  Environ.env ->
  Evd.evar_map ->
  alias list ->
  EConstr.constr ->
  EConstr.constr

Source

val noccur_evar : 
  Environ.env ->
  Evd.evar_map ->
  Evar.t ->
  EConstr.constr ->
  bool

Sourceexception IllTypedInstance of Environ.env * EConstr.types * EConstr.types

Source

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

Sourceval remove_instance_local_defs : Evd.evar_map -> Evar.t -> 'a list -> 'a list

Source

val get_type_of_refresh : 
  ?polyprop:bool ->
  ?lax:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Evd.evar_map * EConstr.types

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Evarsolve/index.html

Module `Evarsolve`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Evarsolve/index.html

Module EvarsolveSource

Module `Evarsolve`Source