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 /pretyping/unification.mli | |
| 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 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0f5a62bb5..ce74852d3 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,6 +13,7 @@ open Evd type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly_in_conv_on_closed_terms : bool; + use_evars_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; check_applied_meta_types : bool; |