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