port to rocq 9

[damien-pous]

tentative version for rocq 9
we had either to use -deprecated-from-Coq, or to rename the corresponding imports.
since we had to do a new version anyways, I did the latter.
I've also added the changes that were pending in coq-community branches, I hope this is ok

[palmskog]

@damien-pous can we please not merge this into master? The right way to do this is that I make a v9.0 branch, and then this PR should target that branch instead.

[palmskog]

@damien-pous I changed the PR to target v9.0, but there are a lot of things here that break CI and other boilerplate. Do you think you could change your repo branch so that only the .v file changes are included? Then I could do the the CI/boilerplate changes separately.

[damien-pous]

Will try...

[palmskog]

If it's too much work, you could also make a new branch in your own repo based on the current v9.0 branch here and then add your .v file changes there (and open a new PR and close this one).

[damien-pous]

I'll probably do that: I've tried something but it does not longer compile (can't see why), and we would get very weird commit history if we continue with this PR.
I have to go so I'll continue this tomorrow.

[palmskog]

I think the problem is you still the need the following diff to compile:

diff --git a/_CoqProject b/_CoqProject
index cf13fea..cb7f43e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,6 @@
 -I src
 
 -arg -w -arg +default
--arg -w -arg -deprecated-from-Coq
 
 src/coq.mli
 src/helper.mli

But feel free to push this tomorrow and I can take over from there.

[palmskog]

As to the commit history, I can do a squash merge so the unneeded changes disappear.

[damien-pous]

Hi @palmskog,

The problem was just that I was trying to compile with make... instead of dune.
My last commit compiles ; it's not on .v files (dune for a warning, _CoqProject since we do not need -deprecated-from-Coq anymore, and meta.yml to be consistent in the doc).

There is still a dune warning about Coq language version, which I have not clue how to fix.

[palmskog]

There is no need to fix the Dune warning, I'll take it from here and merge.

[damien-pous]

great, thanks!