path: root/test-suite/bugs/closed/bug_13300.v

Polymorphic Definition type := Type.

Inductive bad : type := .

Fail Check bad : Prop.
Check bad : Set.
(* lowered as much as possible *)