aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_11421.v
blob: 8ddf05c8886b0a6a23ad115ef4f9ccd1ecdacae8 (plain)
1
Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}.