| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | In evarconv and unification, expand folded primitive projections to |  Matthieu Sozeau | 2014-09-29 |
| | | | | | | | | | | | their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly. | ||
| * | Add missing "Fail" to bug cases. |  Xavier Clerc | 2014-09-26 |
| | | |||
| * | Add several reproduction files for bugs. | Xavier Clerc | 2014-09-25 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |