universes.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/failure/universes.v

blob: d708b01ffcbd39c9c15c5b7b6757e69eafdfe50f (plain)

1
2
3

Definition Type2 := Type.
Definition Type1 : Type2 := Type.
Fail Definition Inconsistency : Type1 := Type2.