From c221e1bebd5fabe7c5995c9306b96596026de047 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Jul 2009 12:30:19 +0000 Subject: Reactivation of pattern unification of evars in apply unification, in agreement with wish #2117 (pattern unification of evars remained deactivated for 3 years because of incompatibilities with eauto [see commit 9234]; thanks to unification flags, it can be activated for apply w/o changing eauto). Also add test for bug #2123 (see commit 12228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenvtac.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'proofs') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c3e6e3d87..87dd26779 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -109,6 +109,7 @@ let fail_quick_unif_flags = { use_metas_eagerly = false; modulo_delta = empty_transparent_state; resolve_evars = false; + use_evars_pattern_unification = false; } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -- cgit v1.2.3