aboutsummaryrefslogtreecommitdiffhomepage
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.