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 /proofs/clenvtac.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 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7d25bb665..087ac0c33 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -96,6 +96,7 @@ let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = let fail_quick_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; check_applied_meta_types = false; |