aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5762.v
Commit message (Expand)AuthorAge
* One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
* Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05