search

mit-plv / coqutil

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

Properly deprecate combine and split #59

Closed proux01 closed 2 years ago

proux01 commented 2 years ago

This was discovered while preparing https://github.com/coq/coq/pull/15760

proux01 commented 2 years ago

@JasonGross could you take care of this please? this is the only remaining failure in https://github.com/coq/coq/pull/15760 If you could also take care of the submodules in bedrock2 and fiat_crypto, that would be wonderful (I tend to wreak havoc whenever I touch git submodules).

JasonGross commented 2 years ago

Sure, I'll take care of this PR within the next couple of days. Unfortunately I'll need help from @samuelgruetter @andres-erbsen and/or @jadephilipoom with the submodules in other repositories ; currently rupicola doesn't build on it's own CI, I've had a PR open for a while trying to bump the bedrock2 submodule without success, and it looks like the latest changes in coqutil have already broken bedrock2

JasonGross commented 2 years ago

I just set the CI running, hopefully it'll pass and we can merge

samuelgruetter commented 2 years ago

Just curious, why do you need such a large diff to deprecate two functions? Shouldn't it be possible to do that with just a two-line change?

proux01 commented 2 years ago

The bulky part of the diff is just to avoid deprecation warnings (that were not trigered before because deprecation in Coq only works for notations (and Ltac(2)).

proux01 commented 2 years ago

Rebased, CI should go through now.

proux01 commented 2 years ago

@JasonGross CI green

samuelgruetter commented 2 years ago

Just merged, and I will also bump it in bedrock2 later today!