Turn require Coq depr warnings as error by default

[proux01]

Overlays (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/21851 rocq-community/atbr#48
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 rocq-community/bignums#110
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 mit-plv/fiat#129
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 Mtac2/Mtac2#428
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 rocq-community/paramcoq#155
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 smtcoq/smtcoq#162
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 rocq-community/stalmarck#34
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 UniMath/UniMath#2075
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 stdlib#253
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 mit-plv/rewriter#200
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 LPCIC/coq-elpi#991
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 math-comp/hierarchy-builder#588
• Adapt to https://github.com/proux01/algebra-tactics/pull/new/rocq21851 math-comp/algebra-tactics#130
• Adapt to https://github.com/rocq-prover/rocq/pull/21851 math-comp/analysis#1929

[JasonGross]

What is the reason for this? (Is there any urgency?)

Given the somewhat fluid boundary between corelib and stdlib, it seems much nicer to have a common prefix that can be used to refer to both of them.

I was under the impression that the stdlib split was done somewhat tentatively, with the option to revert it if it seemed to do more harm than good. Has there been a debrief of the impacts of doing the split and which impacts are positive and which are negative?

[proux01]

These deprecations date back from 9.0, planing actual removal in 9.4 is already way offer the official 2 successive versions compatibility policy.

Note that you still have your common require prefix, it's just Stdlib instead of Coq.

[JasonGross]

Dropping compatibility after two versions is fine for changes that are unambiguously positive, but you have not addressed my other question:

Has there been a debrief of the impacts of doing the split and which impacts are positive and which are negative?

[proux01]

That's pretty orthogonal. The Coq -> Stdlib renaming has more to do with the renaming than with the Stdlib library becoming an actual library. And whatever happens to Stdlib in the future, it's unlikely we'll ever rename it Coq.

Even if you disagree, this is not yet removing the deprecation so you have one more release cycle to trigger any discussion you want to have.

[SkySkimmer]

This seems like another case where the as-error step is useless. IMO we can leave this as a normal warning for a while longer.

[proux01]

I disagree on this one. As a user I'd prefer to have an error by default warning (that I can easily silence) and later don't even notice the change because I'd probably have adapted by then than forgeting about the warning and later getting a more surprising error that I have no choice but to adapt "immediatly".