revert references from Corelib to Coq, simplify build

[hoheinzollern]

Motivation for this change

fixes #1612

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I have pinged @proux01 because how simple these things could seem it appears that in practice the unexpected is to be expected ^_^

[proux01]

We shouldn't do anything like that until we drop support for 8.20 (probably in about 6 months), otherwise compilation without Stdlib (on Rocq >= 9.0) cannot be tested and will easily become broken.

[proux01]

Now that CI is fixed, we clearly see that we can't do that. Should we close?
Note that if you find the thing annoying, the best solution is probably to work on 9.0 rather than 8.20 (it's better performancewise anyway).

[hoheinzollern]

Thanks @proux01 for checking this out. You clearly have a better grasp of all the combinations and possible failures, so it makes sense to drop the PR. Could you add an explanation on the related issue for why this is not viable?

My motivation for trying this is that changing source files in the build script is confusing especially for newcomers, and these changes find their ways into PRs which need to be cleaned up. Plus this doc page made me believe that the compatibility namespace would work under all combinations. It is also annoying when your setup triggers a complete remake, but as you say, that can be circumvented by choosing a different setup.

[proux01]

Could you add an explanation on the related issue for why this is not viable?

Done

Plus this doc page made me believe that the compatibility namespace would work under all combinations.

Unfortunately, only when you keep depending on Stdlib which we don't.

It is also annoying when your setup triggers a complete remake, but as you say, that can be circumvented by choosing a different setup.

I agree it's annoying. Hopefully we get rid of it in 6 months. Meanwhile, it's fine on 9.0.