Adapt to coq/coq#20150 (more aggressive universe minimization) #3341
Annotations
2 errors and 2 warnings
|
Build HoTT:
theories/Metatheory/Nat.v#L823
Universe instance length for equiv_unit_rec is 1 but should be 2.
|
|
Build HoTT:
theories/Idempotents.v#L761
Universe instance length for split_idem is 2 but should be 3.
|
|
Build HoTT:
theories/Basics/Settings.v#L10
"coq-core" has been renamed to "rocq-runtime".
|
|
Build HoTT:
theories/Basics/Settings.v#L12
"coq-core" has been renamed to "rocq-runtime".
|
Loading