aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity/autodecomp.v
Commit message (Expand)AuthorAge
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26