Adapt w.r.t. coq/coq#16004.

[ppedrot]

Should be backwards compatible.

[ppedrot]

Not sure what is the policy for older versions. I'm a bit surprised that mathclasses still compiles with 8.6, is this really true?

[spitters]

I don't recall dropping support for 8.6 to 8.10, but it looks like the nix file only tests from 8.11, which would be fine with me.

[ppedrot]

I've pushed a patch to be more compatible with older versions, by deactivating the unknown attribute warning. Let's see how it fares, if it compiles up to 8.11 it should be good to go.

[spitters]

Thanks! It works from 8.11.
We should probably disable the other builds in CI.

[ppedrot]

OK, so I consider this ready to merge. Deactivating the broken CIs should be performed in its own PR, instead.

[Zimmi48]

We had dropped compatibility with Coq versions < 8.11 in 8.13.0, but it was reintroduced by a contributor in 8.15.0. It's fine to remove it now. Removing the tests with Coq 8.6-8.10 should amount to reverting #103 (except that there will be a conflict in meta.yml and the opam file).

[ppedrot]

AFAICT even in master these tests are broken. If you look at the output of the CI in this PR, there is already an issue with the Automatic Introduction flag which is unrelated to the patches from here.

[ppedrot]

@spitters ping

[spitters]

Thanks! I'll merge this, @Zimmi48 if you have time, could you send a PR to reverse #103 ?