Packages should list the compatible Coq version(s) everywhere

[palmskog]

Due to so many Coq opam archive packages being old, and therefore not compatible with recent Coq, every listing of a package should reasonably include the Coq version constraint (if there is one, e.g., packages depending on coq-mathcomp-ssreflect sometimes do not add this).

[gares]

At least for packages in the mathcomp main repo, there was a deliberate choice to delegate this task to the root package, that (used to be) the only one really tied to a Coq version because of its .ml code. That code is now gone, so we may reconsider that policy.

But I think that using opam's meta data for this specific task (telling a user if package X works with Coq version V) is a not ideal.
If a package X declares compat with version V, we are not systematically amending packages if the package happens to be also compatible with V+1. Ideally a bot would do that. The converse also holds, if we stop putting an upper bound and no bot tells us that some upper bound should be put, we will end up claiming something false.

[silene]

I think we could use a conservative approach, that is, display the upper bound on Coq only if it exists. For instance, the following tells which Coq version is required, and if it differs from the most recent release, then it could be displayed.

opam install --dry-run --update-invariant coq-foobar | grep -e "install *coq "

(I am not necessarily suggesting to do it that way. It would presumably be more robust to write a small OCaml script that uses the API of Opam.)