| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merge branch 'v8.6' |  Pierre-Marie Pédrot | 2017-05-17 |
| |\ | |||
| | * | remove unneeded -emacs flag to coq-prog-args |  Paul Steckler | 2017-05-01 |
| | | | |||
| * | | Moving the Ltac plugin to a pack-based one. | Pierre-Marie Pédrot | 2017-02-17 |
| |/ | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements. | ||
| * | Fix minimization to be insensitive to redundant arcs. |  Matthieu Sozeau | 2016-10-20 |
| | | | | | | | | | | | | | | | | | The new algorithm produces different sets of arcs than in 8.5, hence existing developments may fail to pass now because they relied on the (correct but more approximate) result of minimization in 8.5 which wasn't insensitive. The algorithm works bottom-up on the (well-founded) graph to find lower levels that an upper level can be minimized to. We filter said lower levels according to the lower sets of the other levels we consider. If they appear in any of them then we don't need their constraints. Does not seem to have a huge impact on performance in HoTT, but this should be evaluated further. Adapt test-suite files accordingly. | ||
| * | Add fixed test-suite file for bug #4527 | Matthieu Sozeau | 2016-09-27 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |