Adapt to coq/coq#20150 (more aggressive universe minimization) #3341
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
theories/Metatheory/Nat.v#L823
Universe instance length is 1 but should be 2.
Command exited with non-zero status 1
|
Loading