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. |