diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-08 12:30:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-08 12:30:19 +0000 |
| commit | c221e1bebd5fabe7c5995c9306b96596026de047 (patch) | |
| tree | 53280496702a666b4fc6f98dbf7499afccc80ab4 /pretyping/unification.mli | |
| 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/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 8d71ec4bd..43c9dd2e9 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 |