aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2080.v
Commit message (Expand)AuthorAge
* Removing test for bug #2080.Gravatar Pierre-Marie Pédrot2014-10-01
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10