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

val w_unify : Environ.env -> Evd.evar_map -> Evd.conv_pb -> ?flags:unify_flags -> EConstr.constr -> EConstr.constr -> Evd.evar_map

The "unique" unification function

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

val w_unify_meta_types : Environ.env -> ?flags:unify_flags -> Evd.evar_map -> Evd.evar_map

val w_coerce_to_type : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types -> EConstr.types -> Evd.evar_map * EConstr.constr

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 * EConstr.constr * Locus.clause * bool

| AbstractExact of Names.Name.t * EConstr.constr * EConstr.types option * Locus.clause * bool

type 'r abstraction_result = Names.Id.t * Environ.named_context_val * EConstr.named_declaration list * Names.Id.t option * EConstr.types * (Evd.evar_map * EConstr.constr) option

val make_abstraction : Environ.env -> Evd.evar_map -> EConstr.constr -> abstraction_request -> 'r abstraction_result

val pose_all_metas_as_evars : Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

val abstract_list_all : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr list -> Evd.evar_map * (EConstr.constr * EConstr.types)

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)

type metabinding = Constr.metavariable * EConstr.constr * (Evd.instance_constraint * Evd.instance_typing_status)

type subst0 = Evd.evar_map * metabinding list * ((Environ.env * int) * EConstr.existential * EConstr.t) list

val w_merge : Environ.env -> bool -> core_unify_flags -> subst0 -> Evd.evar_map

val unify_0 : Environ.env -> Evd.evar_map -> Evd.conv_pb -> core_unify_flags -> EConstr.types -> EConstr.types -> subst0