diff options
| author | herbelin | 2009-07-08 12:30:19 +0000 |
|---|---|---|
| committer | herbelin | 2009-07-08 12:30:19 +0000 |
| commit | c221e1bebd5fabe7c5995c9306b96596026de047 (patch) | |
| tree | 53280496702a666b4fc6f98dbf7499afccc80ab4 /pretyping | |
| parent | cb0a4dbc77da083e866e88523dc30244b1e25117 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 9 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 |
2 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8ea2eae11b..0846359a85 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -128,6 +128,7 @@ type unify_flags = { use_metas_eagerly : bool; modulo_delta : Names.transparent_state; resolve_evars : bool; + use_evars_pattern_unification : bool } let default_unify_flags = { @@ -135,6 +136,7 @@ let default_unify_flags = { use_metas_eagerly = true; modulo_delta = full_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let default_no_delta_unify_flags = { @@ -142,6 +144,7 @@ let default_no_delta_unify_flags = { use_metas_eagerly = true; modulo_delta = empty_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let expand_key env = function @@ -229,12 +232,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 | App (f1,l1), _ when - isMeta f1 & is_unification_pattern curenvnb f1 l1 cN & + (isMeta f1 || flags.use_evars_pattern_unification && isEvar f1) & + is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> solve_pattern_eqn_array curenvnb f1 l1 cN substn | _, App (f2,l2) when - isMeta f2 & is_unification_pattern curenvnb f2 l2 cM & + (isMeta f2 || flags.use_evars_pattern_unification && isEvar f2) & + is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> solve_pattern_eqn_array curenvnb f2 l2 cM substn diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 8d71ec4bd6..43c9dd2e9b 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -19,6 +19,7 @@ type unify_flags = { use_metas_eagerly : bool; modulo_delta : Names.transparent_state; resolve_evars : bool; + use_evars_pattern_unification : bool } val default_unify_flags : unify_flags |