aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3228.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2014-04-05Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Hugo Herbelin