search

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

Stop relying on `replace by` automatic `assumption`-based solving #371

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

Before coq/coq#17964 replace foo with bar by tac actually means replace foo with bar by first [assumption | symmetry; assumption | tac].