diff options
author | 2014-09-02 19:27:50 +0200 | |
---|---|---|
committer | 2014-09-10 15:26:52 +0200 | |
commit | bcd144642c5f23a69ac96afe3a9f3ae370fcfa96 (patch) | |
tree | 8d7dd7921cbeddbe111d856174f7bfde27fc7455 /proofs | |
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 'proofs')
-rw-r--r-- | proofs/clenv.ml | 2 | ||||
-rw-r--r-- | proofs/clenvtac.ml | 13 |
2 files changed, 10 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 33df4ca97..c6f0f2ee0 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -360,7 +360,7 @@ let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv = env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = - clenv_unify ~flags:flags CUMUL + clenv_unify ~flags CUMUL (clenv_term clenv' nextclenv.templtyp) (clenv_meta_type clenv' mv) clenv' in diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index d4826ce20..94731b039 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -93,21 +93,26 @@ let res_pf ?(with_evars=false) ?(flags=dft ()) clenv = d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) -let fail_quick_unif_flags = { +let fail_quick_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; - modulo_delta_in_merge = None; check_applied_meta_types = false; - resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) frozen_evars = Evar.Set.empty; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; - allow_K_in_toplevel_higher_order_unification = false +} + +let fail_quick_unif_flags = { + core_unify_flags = fail_quick_core_unif_flags; + merge_unify_flags = fail_quick_core_unif_flags; + subterm_unify_flags = fail_quick_core_unif_flags; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) |