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

Use List.Forall2_nil instead of List.Forall2_refl #386

Closed SkySkimmer closed 11 months ago

SkySkimmer commented 11 months ago

Forall2_refl is deprecated due to its type not matching its name (it's only about nil), Forall2_nil having the same type.

samuelgruetter commented 11 months ago

Looks like this is an easy one to merge, for once :wink: Thanks for all your work to keep Bedrock2 compatible :+1: