Adapt to coq/coq#20150 (more aggressive universe minimization) #3341
Annotations
2 errors
|
Build HoTT:
theories/Metatheory/Nat.v#L823
Universe instance length is 1 but should be 2.
|
|
Build HoTT:
theories/Idempotents.v#L761
Universe instance length is 2 but should be 3.
|
Loading