Adapt to https://github.com/coq/coq/pull/19530

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 https://github.com/coq/coq/pull/19530 #432

Open proux01 opened 1 month ago

proux01 commented 1 month ago

Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future). Merging this is not required for the upstream PR, you can do whatever you want with it.