diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 15 |
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; |