aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_13495.v
AgeCommit message (Expand)Author
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau