aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity/autodecomp.v
AgeCommit message (Expand)Author
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2009-03-04illegal tactic application was having Ltac interpreter loopbarras
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin