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 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
type abstraction_request =
| AbstractPattern of prefix_of_inductive_support_flag
* EConstr.types ->
bool
* Names.Name.t
* Evd.evar_map option * 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