| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-19 | An optimization of tactic constructor. | Hugo Herbelin | |
| 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 formal proof system |
| aboutsummaryrefslogtreecommitdiff |