Remove deprecated files in Coq.Arith

[Villetaneuse]

Necessary for coq/coq#18164

[Villetaneuse]

@JasonGross This should be ok, I think.

[JasonGross]

@Villetaneuse I don't have permissions on this repository, I think we need @samuelgruetter @andres-erbsen here

[JasonGross]

Also, btw, if you write it as coq/coq#18164 (without the :), I think GitHub will autolink the issue

[Villetaneuse]

Also, btw, if you write it as coq/coq#18164 (without the :), I think GitHub will autolink the issue

Sorry, still quite new to this. This is edited. And thank you for the correct pings!

[samuelgruetter]

In Coq 8.15, this fails with

Error: The reference Even_Odd_dec was not found in the current environment.

But, as far as I understand, the bbv library is not really used any more, except maybe for rebuilding old projects, so before anyone spends time on making it compatible with several Coq versions, maybe we should ask if we should simply take bbv out of Coq's CI?

[Villetaneuse]

In Coq 8.15, this fails with

Error: The reference Even_Odd_dec was not found in the current environment.

But, as far as I understand, the bbv library is not really used any more, except maybe for rebuilding old projects, so before anyone spends time on making it compatible with several Coq versions, maybe we should ask if we should simply take bbv out of Coq's CI?

Thank you, I don't know who decides such things. I'm putting a link to your post on zulip here.

[JasonGross]

It's used by fiat-crypto-legacy, which I'd like to keep compatible in Coq's CI, but for which multiple version compatibility is also not important, so maybe it's best to bump bbv's CI to test 8.16, 8.17, 8.18, master?

[samuelgruetter]

so maybe it's best to bump bbv's CI to test 8.16, 8.17, 8.18, master?

I just tried that, but it seems 8.18 is not yet available in the Ubuntu builds. Should I just do 8.16, 8.17 & master for now @JasonGross ?

[JasonGross]

Yes, that sounds good. I'll try to get 8.18 in Ubuntu packaging soon

[samuelgruetter]

Ok so I just pushed CI for 8.16, 8.17 & Coq master to bbv's master.
@Villetaneuse could you please rebase this PR?

[Villetaneuse]

Ok so I just pushed CI for 8.16, 8.17 & Coq master to bbv's master. @Villetaneuse could you please rebase this PR?

Done.

[Villetaneuse]

@samuelgruetter thank you very much!