aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/universes.v
blob: 938c29b839dfbd43f011ad2961e4c6a49e6cc9db (plain)
1
2
3
Definition Type2 := Type.
Definition Type1 : Type2 := Type.
Definition Inconsistency : Type1 := Type2.