aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4932.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Fixing #4932 (anomaly when using binders as terms in recursive notations).Hugo Herbelin