aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4869.v
blob: 6d21b66fe97533f054bbfeaa5ae93f5f0975f76f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Universes i.

Fail Constraint i < Set.
Fail Constraint i <= Set.
Fail Constraint i = Set.
Constraint Set <= i.
Constraint Set < i.
Fail Constraint i < j. (* undeclared j *)
Fail Constraint i < Type. (* anonymous *)

Set Universe Polymorphism.

Section Foo.
  Universe j.
  Constraint Set < j.

  Definition foo := Type@{j}.
End Foo.