blob: 0350be9c0605d13d67c24d6aec56e6ceb5ffaf64 (
plain)
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 *)
|