| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | An optimization of tactic constructor. |  Hugo Herbelin | 2017-09-19 |
| As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |