[coq] 1.0 version coq language version meta-issue

Here is a list of missing items toward a (using coq 1.0) beta and stable release.

I separated issues on two kinds: issues that need to be resolved before we can do a wide call for testing / porting in the Coq community, and issues that are required for 1.0 but not for the beta.

Beta-blocking issues:

• inter-scope composition of theories, including support for installed theories (so people can port opam packages to Dune)
  c.f https://github.com/ocaml/dune/pull/5784 and maybe some extra PR
• Better coq native support (#5831)

With the above in place, quite a lot of packages could be permanently ported to Dune and release in opam this way.

For 1.0, it'd be nice to have too:

• Add a %{coq_version} variable so people can have conditional copy rules for those that need compat with older Coq https://github.com/ocaml/dune/pull/6049
• coqchk support
• check that our coqdoc system is OK for usres
• sharing of (include_subdirs ...) between Coq and OCaml is quite inconvenient for a few users c.f. https://github.com/ocaml/dune/issues/3314 https://github.com/ocaml/dune/issues/2857
• https://github.com/ocaml/dune/issues/4158
• resolve https://github.com/ocaml/dune/issues/2585

Review the remaining unchecked Coq 1.0 items and the linked issues #3314, #2857, #4158, and #2585, alongside the completed PRs #5784 and #6049. Done means the listed beta and 1.0 requirements are resolved and the project is ready for the stated Coq release goals; no source files or tests are named here.