Skip to content

Adapt to rocq-prover/rocq#21833.#197

Merged
andres-erbsen merged 1 commit intomit-plv:masterfrom
ppedrot:rm-non-global-hint
Mar 30, 2026
Merged

Adapt to rocq-prover/rocq#21833.#197
andres-erbsen merged 1 commit intomit-plv:masterfrom
ppedrot:rm-non-global-hint

Conversation

@ppedrot
Copy link
Copy Markdown
Contributor

@ppedrot ppedrot commented Mar 28, 2026

Should be backwards compatible.

@ppedrot
Copy link
Copy Markdown
Contributor Author

ppedrot commented Mar 30, 2026

(ping @andres-erbsen just in case since you merged the other overlays on fiat-crypto.)

@andres-erbsen
Copy link
Copy Markdown
Contributor

I believe the CI failure is unrelated and will merge on that basis.

@andres-erbsen andres-erbsen merged commit 487232d into mit-plv:master Mar 30, 2026
8 of 10 checks passed
@ppedrot
Copy link
Copy Markdown
Contributor Author

ppedrot commented Mar 30, 2026

Thanks!

@ppedrot ppedrot deleted the rm-non-global-hint branch March 30, 2026 18:24
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