aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5762.v
AgeCommit message (Expand)Author
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin