summaryrefslogtreecommitdiff
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 06:54:52 +0000