aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5470.v
AgeCommit message (Expand)Author
2017-04-14Fixing bug #5470 (anomaly on notations with misused "binder" type).Hugo Herbelin