diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-02 19:27:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-10 15:26:52 +0200 |
| commit | bcd144642c5f23a69ac96afe3a9f3ae370fcfa96 (patch) | |
| tree | 8d7dd7921cbeddbe111d856174f7bfde27fc7455 /pretyping/unification.mli | |
| parent | af767e36829ada2b23f5d8eae631649e865392ae (diff) | |
A step towards better differentiating when w_unify is used for subterm
selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.
No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index de8eecc27..bedd6bf16 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -10,23 +10,31 @@ open Term open Environ open Evd -type unify_flags = { +type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; - modulo_delta_in_merge : Names.transparent_state option; check_applied_meta_types : bool; - resolve_evars : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; frozen_evars : Evar.Set.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; - allow_K_in_toplevel_higher_order_unification : 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 : unit -> unify_flags @@ -79,14 +87,14 @@ val abstract_list_all : (* For tracing *) -val w_merge : env -> bool -> unify_flags -> evar_map * +val w_merge : env -> bool -> core_unify_flags -> evar_map * (metavariable * constr * (instance_constraint * instance_typing_status)) list * (env * types pexistential * types) list -> evar_map val unify_0 : Environ.env -> Evd.evar_map -> Evd.conv_pb -> - unify_flags -> + core_unify_flags -> Term.types -> Term.types -> Evd.evar_map * Evd.metabinding list * @@ -98,7 +106,7 @@ val unify_0_with_initial_metas : bool -> Environ.env -> Evd.conv_pb -> - unify_flags -> + core_unify_flags -> Term.types -> Term.types -> Evd.evar_map * Evd.metabinding list * |