aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_sprop_14.v
AgeCommit message (Expand)Author
2019-03-14Add a non-cumulative impredicative universe SProp.Gaƫtan Gilbert