| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Follow up to experimental eager evar unification in bcba6d1bc9: |  Hugo Herbelin | 2014-11-08 |
| 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). | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |