Skip to content

Conversation

@yforster
Copy link
Member

@SkySkimmer this should fix Coq master again

@yforster
Copy link
Member Author

I accidentally changed the CI to use coq-8.18 in this merge, that's why we didn't catch the incompatibility with Coq master -- now that's fixed as well

@JasonGross
Copy link
Contributor

The opam files also need to be updated, eg,
https://github.com/MetaCoq/metacoq/blob/adc980ccf69be29be24db632de9ac8321ad54d44/coq-metacoq-utils.opam#L32
needs to permit dev

@yforster
Copy link
Member Author

Thanks @JasonGross!

@yforster
Copy link
Member Author

Still erroring in CI, but I think this error we've had before my merge as well? Good to merge into main @SkySkimmer?

@SkySkimmer
Copy link
Contributor

I don't know why you're asking me tbh

@JasonGross
Copy link
Contributor

I think this should be merged. I expect MetaCoq to still fail on Coq master with this universe error on vos mode, which I think is possibly a regression Coq-side. MetaCoq
CI side this can be fixed by disabling vos for whichever component is failing, which I seem to recall having to do for some part of quotation already.

@yforster yforster merged commit 64ce785 into main Oct 17, 2023
@yforster yforster deleted the main-elimtype branch October 17, 2023 15:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants