We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse.
The first error message is:
coqc TypeTheory/TypeTheory/Auxiliary/Auxiliary.{glob,vo} (exit 1) File "./TypeTheory/TypeTheory/Auxiliary/Auxiliary.v", line 15, characters 0-43: Error: Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because PartA.cast.u1 <= PartA.cast.u0 < UU.u0.
The text was updated successfully, but these errors were encountered:
No branches or pull requests
In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse.
The first error message is:
coqc TypeTheory/TypeTheory/Auxiliary/Auxiliary.{glob,vo} (exit 1) File "./TypeTheory/TypeTheory/Auxiliary/Auxiliary.v", line 15, characters 0-43: Error: Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because PartA.cast.u1 <= PartA.cast.u0 < UU.u0.The text was updated successfully, but these errors were encountered: