aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml4
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-18 20:35:22 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-18 20:35:22 +0000
commit9d7499dcd4440aca458cb190ed108ae9b3adff17 (patch)
tree600b19fc9ca74cb6149676276b670e731e12ae66 /tactics/rewrite.ml4
parentc79db26e91c61bfa085e667ae14733a463b73423 (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/rewrite.ml4')
-rw-r--r--tactics/rewrite.ml415
1 files changed, 9 insertions, 6 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 821284ec7..5400827bc 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -302,11 +302,12 @@ let rewrite_transparent_state () =
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 = full_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;
@@ -316,11 +317,12 @@ let rewrite_unif_flags = {
let rewrite2_unif_flags =
{ Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
- 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 = conv_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 = true;
@@ -331,11 +333,12 @@ let rewrite2_unif_flags =
let general_rewrite_unif_flags () =
let ts = rewrite_transparent_state () in
{ Unification.modulo_conv_on_closed_terms = Some ts;
- Unification.use_metas_eagerly = true;
+ Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
Unification.modulo_delta = ts;
Unification.modulo_delta_types = ts;
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 = true;