Commit 4cc2df2
Pulls in mit-plv/rewriter's adaptation to the removal of the
deprecated coq-core.* findlib library aliases
(rocq-prover/rocq#21955), merged as
mit-plv/rewriter#203.
Without this, the dev (rocq dev / 9.3) docker CI builds fail while
compiling the rewriter submodule with:
*** Error: In file src/Rewriter/Util/plugins/RewriterBuild.v
findlib error: coq-core.plugins.ltac not found
...
required by `coq-rewriter.rewriter_build'
because the rewriter META still required coq-core.plugins.* which no
longer exists on rocq 9.3. The bumped rewriter generates the META
per Coq version (coq-core.* on 8.x/9.0-9.2, rocq-runtime.* on 9.3).
https://claude.ai/code/session_01PjCbMk9zjAZWvZHuznFXqh
Co-authored-by: Claude <noreply@anthropic.com>
1 parent 901b3fb commit 4cc2df2
1 file changed
Lines changed: 1 addition & 1 deletion
- .gitignore+1
- Makefile+2-2
- Makefile.local-late+4
- Makefile.local.common+1-2
- _CoqProject.in+1-1
- etc/coq-scripts+1-1
- src/Rewriter/Util/GlobalSettings.v+1
- src/Rewriter/Util/plugins/META.coq-rewriter.v815
- src/Rewriter/Util/plugins/META.coq-rewriter.v816
- src/Rewriter/Util/plugins/META.coq-rewriter.v817+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v818+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v819+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v820+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v821+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v90+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v91+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v92+46
- src/Rewriter/Util/plugins/META.coq-rewriter.v93+46
0 commit comments