Module Unification

Meta machinery

These functions are almost deprecated. They were used before the introduction of the full-fledged evar calculus. In an ideal world, they should be removed. Alas, some parts of the code still use them. Do not use in newly-written code.

module Metaset : Util.Set.S with type elt = Constr.metavariable
module Metamap : Util.Map.ExtS with type key = Constr.metavariable and module Set := Metaset
type 'a freelisted = private {
rebus : 'a;
freemetas : Metaset.t;
}
val metavars_of : Evd.econstr -> Metaset.t
module Meta : sig ... end

Metas

Legacy unification
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
use_evars_eagerly_in_conv_on_closed_terms : bool;
modulo_delta : TransparentState.t;
modulo_delta_types : TransparentState.t;
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
allowed_evars : Evarsolve.AllowedEvars.t;
restrict_conv_on_strict_subterms : bool;
modulo_betaiota : bool;
modulo_eta : bool;
}
type unify_flags = {
core_unify_flags : core_unify_flags;
merge_unify_flags : core_unify_flags;
subterm_unify_flags : core_unify_flags;
allow_K_in_toplevel_higher_order_unification : bool;
resolve_evars : bool;
}
val default_core_unify_flags : unit -> core_unify_flags
val default_no_delta_core_unify_flags : unit -> core_unify_flags
val default_unify_flags : unit -> unify_flags
val default_no_delta_unify_flags : TransparentState.t -> unify_flags
val elim_flags : unit -> unify_flags
val elim_no_delta_flags : unit -> unify_flags
val is_keyed_unification : unit -> bool

The "unique" unification function

val w_unify_to_subterm : ?metas:Meta.t -> Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Meta.t * Evd.evar_map) * EConstr.constr

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.

val w_unify_to_subterm_all : ?metas:Meta.t -> Environ.env -> Evd.evar_map -> ?flags:unify_flags -> (EConstr.constr * EConstr.constr) -> (Meta.t * Evd.evar_map) list
val w_unify_meta_types : ?metas:Meta.t -> Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Meta.t * 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

exception PatternNotFound
type prefix_of_inductive_support_flag = bool
type abstraction_request =
| AbstractPattern of prefix_of_inductive_support_flag * EConstr.types -> bool * Names.Name.t * Evd.evar_map option * EConstr.constr * Locus.clause
| AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool
val pose_all_metas_as_evars : metas:Meta.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * Meta.t * EConstr.constr

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)