From bcd144642c5f23a69ac96afe3a9f3ae370fcfa96 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 2 Sep 2014 19:27:50 +0200 Subject: 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). --- proofs/clenvtac.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'proofs/clenvtac.ml') 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)) *) -- cgit v1.2.3