Skip to content

new version of coq-mtac2 to 2.1.4+9.1#3753

Open
Justme0606 wants to merge 2 commits into
rocq-prover:masterfrom
Justme0606:mtac2-v1.4-rocq9.1
Open

new version of coq-mtac2 to 2.1.4+9.1#3753
Justme0606 wants to merge 2 commits into
rocq-prover:masterfrom
Justme0606:mtac2-v1.4-rocq9.1

Conversation

@Justme0606

Copy link
Copy Markdown
Contributor

No description provided.

@silene

silene commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

This fails to compile:

CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInit.ml
File "src/metaCoqInit.mlg", line 122, characters 3-12:
Error: Unbound constructor "ProofMode"

I think the ProofMode constructor was introduced in Rocq 9.1, which means that there should be a constraint "coq-core" (>= "9.1") instead of "coq" (>= "9.0"). (And it would make sense, given the name of the tarball.)

But note that Unicoq, which is a dependency, is currently marked as incompatible with Rocq 9.1. So, either a new release of Unicoq is needed, or the current one needs some relaxed bounds.

@Justme0606 Justme0606 force-pushed the mtac2-v1.4-rocq9.1 branch from 7e95a8d to c26fa87 Compare June 17, 2026 14:05
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.

2 participants