mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Adapt to coq/coq#17836 (sort poly) (coqutil update) #374

Closed SkySkimmer closed 11 months ago

SkySkimmer commented 1 year ago

cf https://github.com/mit-plv/coqutil/pull/95

ppedrot commented 11 months ago

Please merge now.

JasonGross commented 11 months ago

We should instead instruct dependabot to recreate https://github.com/mit-plv/bedrock2/pull/384 and then set that to merge

ppedrot commented 11 months ago

This can be closed now, right?