aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity/injection.v
Commit message (Expand)AuthorAge
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* Ajout d'un test de complexité de injection (cf bug 1173)Gravatar herbelin2007-04-14