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 /proofs/clenvtac.ml | |
| 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/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 13 |
1 files changed, 9 insertions, 4 deletions
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)) *) |