test-suite/bugs/closed/8288.v


1
2
3
4
5
6
7

Set Universe Polymorphism.
Set Printing Universes.

Set Polymorphic Inductive Cumulativity.

Inductive foo := C : (forall A : Type -> Type, A Type) -> foo.
(* anomaly invalid subtyping relation *)