diff options
| author | herbelin | 2011-06-18 20:35:22 +0000 |
|---|---|---|
| committer | herbelin | 2011-06-18 20:35:22 +0000 |
| commit | 9d7499dcd4440aca458cb190ed108ae9b3adff17 (patch) | |
| tree | 600b19fc9ca74cb6149676276b670e731e12ae66 /tactics/equality.ml | |
| parent | c79db26e91c61bfa085e667ae14733a463b73423 (diff) | |
Generalizing flag use_evars_pattern_unification into a flag
use_pattern_unification common for evars and metas. As a compensation,
add a flag use_meta_bound_pattern_unification to restore the old
mechanism of pattern unification for metas applied to rels only (this
is used e.g. by auto). Not sure yet, what could be the most
appropriate set of flags. Added documentation of the flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index d2970603ea..3a40994f8c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -82,11 +82,12 @@ type conditions = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; Unification.resolve_evars = true; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; + Unification.use_meta_bound_pattern_unification = true; Unification.frozen_evars = ExistentialSet.empty; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; @@ -142,17 +143,19 @@ let rewrite_conv_closed_unif_flags = { (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) - Unification.use_metas_eagerly = true; + Unification.use_metas_eagerly_in_conv_on_closed_terms = true; (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.resolve_evars = false; - Unification.use_evars_pattern_unification = true; + Unification.use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) (* a preexisting evar of the goal*) + Unification.use_meta_bound_pattern_unification = true; + Unification.frozen_evars = ExistentialSet.empty; (* This is set dynamically *) |