aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5755.v
AgeCommit message (Expand)Author
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin