Skip to content

Add overlay for #21098#107

Merged
proux01 merged 1 commit into
rocq-community:masterfrom
tabareau:sortpoly-equality
Oct 20, 2025
Merged

Add overlay for #21098#107
proux01 merged 1 commit into
rocq-community:masterfrom
tabareau:sortpoly-equality

Conversation

@tabareau

@tabareau tabareau commented Oct 20, 2025

Copy link
Copy Markdown
Contributor

Adapt to rocq-prover/rocq#21098
Use rewrite_strat instead of autorewrite to speed compilation time up

@proux01 proux01 marked this pull request as draft October 20, 2025 14:29
@proux01

proux01 commented Oct 20, 2025

Copy link
Copy Markdown
Collaborator

Apparently not backward compatible, will have to be merged in sync with upstream PR I guess?

@tabareau

Copy link
Copy Markdown
Contributor Author

Now it should be

@proux01 proux01 marked this pull request as ready for review October 20, 2025 15:09
@proux01 proux01 merged commit 05e6ab6 into rocq-community:master Oct 20, 2025
1 check passed
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