blob: 8baaf8686ad1fc46ed6412efc6fd785391e9ad7a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Set Universe Polymorphism.
Set Printing Universes.
Unset Strict Universe Declaration.
Monomorphic Universe v.
Section Foo.
Let bar := Type@{u}.
Fail Monomorphic Constraint bar.u < v.
End Foo. (* was anomaly undeclared universe due to the constraint *)
|
