diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 6da110139..52f10d46c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -283,6 +283,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let conv_transparent_state = (Idpred.empty, Cpred.full) @@ -292,6 +293,7 @@ let rewrite2_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let setoid_rewrite_unif_flags = { @@ -299,6 +301,7 @@ let setoid_rewrite_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = conv_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let convertible env evd x y = |