package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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

Module UnificationSource

Sourcetype core_unify_flags = {
  1. modulo_conv_on_closed_terms : TransparentState.t option;
  2. use_metas_eagerly_in_conv_on_closed_terms : bool;
  3. use_evars_eagerly_in_conv_on_closed_terms : bool;
  4. modulo_delta : TransparentState.t;
  5. modulo_delta_types : TransparentState.t;
  6. check_applied_meta_types : bool;
  7. use_pattern_unification : bool;
  8. use_meta_bound_pattern_unification : bool;
  9. allowed_evars : Evarsolve.AllowedEvars.t;
  10. restrict_conv_on_strict_subterms : bool;
  11. modulo_betaiota : bool;
  12. modulo_eta : bool;
}
Sourcetype unify_flags = {
  1. core_unify_flags : core_unify_flags;
  2. merge_unify_flags : core_unify_flags;
  3. subterm_unify_flags : core_unify_flags;
  4. allow_K_in_toplevel_higher_order_unification : bool;
  5. resolve_evars : bool;
}
Sourceval default_core_unify_flags : unit -> core_unify_flags
Sourceval default_no_delta_core_unify_flags : unit -> core_unify_flags
Sourceval default_unify_flags : unit -> unify_flags
Sourceval default_no_delta_unify_flags : TransparentState.t -> unify_flags
Sourceval elim_flags : unit -> unify_flags
Sourceval elim_no_delta_flags : unit -> unify_flags
Sourceval is_keyed_unification : unit -> bool

The "unique" unification function

w_unify_to_subterm env m (c,t) performs unification of c with a subterm of t. Constraints are added to m and the matched subterm of t is also returned.

Sourceval w_unify_to_subterm_all : Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> Evd.evar_map list
Sourceval w_unify_meta_types : Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Evd.evar_map

w_coerce_to_type env evd c ctyp typ tries to coerce c of type ctyp so that its gets type typ; typ may contain metavariables

Sourceexception PatternNotFound
Sourcetype prefix_of_inductive_support_flag = bool
Sourcetype abstraction_request =
  1. | AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map * EConstr.constr * Locus.clause * bool
  2. | AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool

abstract_list_all env evd t c l abstracts the terms in l over c to get a term of type t (exported for inv.ml)

Sourcetype subst0 = Evd.evar_map * metabinding list * ((Environ.env * int) * EConstr.existential * EConstr.t) list
Sourceval w_merge : Environ.env -> bool -> core_unify_flags -> subst0 -> Evd.evar_map