| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | test-suite: cleaning | Vincent Laporte | |
| 2014-11-08 | Follow up to experimental eager evar unification in bcba6d1bc9: | Hugo Herbelin | |
| 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 formal proof system |
| aboutsummaryrefslogtreecommitdiff |