Module Unification

type allowed_evars =
| AllowAll
| AllowFun of Evar.t -> bool
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 : allowed_evars;
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 * EConstr.constr) 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
val finish_evar_resolution : ?⁠flags:Pretyping.inference_flags -> Environ.env -> Evd.evar_map -> (Evd.evar_map * EConstr.constr) -> Evd.evar_map * EConstr.constr
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 * 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
val unify_0_with_initial_metas : subst0 -> bool -> Environ.env -> Evd.conv_pb -> core_unify_flags -> EConstr.types -> EConstr.types -> subst0