search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

Future proof ZLib.v and div_mod_to_equations.v #35

Closed mrhaandi closed 3 years ago

mrhaandi commented 3 years ago

This PR makes ZLib.v and div_mod_to_equations.v work with https://github.com/coq/coq/pull/14086 in a backwards compatible manner.

samuelgruetter commented 3 years ago

It seems that mod_0_r and mod_pow2_same_cases are not used anywhere in bedrock2, and div_mod_to_equations is now in the standard library, so should not be used any more either, so why not just delete the incompatible code instead of introducing ltac cruft that will break between different Coq versions?

mrhaandi commented 3 years ago

why not just delete the incompatible code instead of introducing ltac cruft that will break between different Coq versions?

coqutil is also used by other projects, so I did not delete anything too eagerly. Of course, coqutil maintainers may delete anything they see as not relevant.