diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 15:28:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-08 17:13:58 +0100 |
| commit | 91c2a866e7827c0ede0539cb49f924b68db569a9 (patch) | |
| tree | a92efd5e411676e34910b54ed58b637bf731dc57 /tactics/auto.ml | |
| parent | c9728f6eba0d4391992e89bdd9886d46fdf16004 (diff) | |
Follow up to experimental eager evar unification in bcba6d1bc9:
Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 18beedf95..43aa84e7a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -43,6 +43,7 @@ open Unification let auto_core_unif_flags_of st1 st2 useeager = { modulo_conv_on_closed_terms = Some st1; use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; check_applied_meta_types = false; |