aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_8794.v
AgeCommit message (Expand)Author
2018-10-23Fixing #8794 (anomaly with abbreviation involving both term and binders).Hugo Herbelin