Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21851#200

Open
proux01 wants to merge 1 commit intomit-plv:masterfrom
proux01:rocq21851
Open

Adapt to https://github.com/rocq-prover/rocq/pull/21851#200
proux01 wants to merge 1 commit intomit-plv:masterfrom
proux01:rocq21851

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Apr 2, 2026

Adapt to rocq-prover/rocq#21851

This should be backward compatible and can be merged without waiting for the upstream PR.

@JasonGross
Copy link
Copy Markdown
Collaborator

This should be backward compatible

This is not backwards compatible with the movement of things between stdlib and corelib

File "./src/Rewriter/Util/FixCoqMistakes.v", line 2, characters 27-36:
Error: Cannot find a physical path bound to logical path
Morphisms with prefix Stdlib.

File "./src/Rewriter/Util/IffT.v", line 1, characters 28-43:
Error: Cannot find a physical path bound to logical path
RelationClasses with prefix Corelib.

@proux01
Copy link
Copy Markdown
Contributor Author

proux01 commented Apr 3, 2026

This is backward compatible down to 9.0. Also note that rewriter is flagged as "plugin" in Rocq CI and we usually only expect those to compile on Rocq master.

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