[coq] auto-infer plugins field

From Coq 8.16 onwards, the plugins field of the coq.theory stanza could be auto-inferred.

1. We find any .v files that do "Declare ML Module".
2. We parse the public_name of the library that is declared.
3. We add this automatically to the list of plugins.

This is only possible from 8.16 onwards as we started using findlib to load plugins. Older versions will not have the plugin names so we need to stay at the current behaviour for those.

This is only about inferring the plugins in the coq.theory stanza and not inferring the plugins in any dependencies. As of writing, Dune is not able to infer the plugins needed from dependencies and this is a bug #7893. The behaviour I am describing here means that a user only has to include a "Declare ML Module" in a .v file rather than having to write them out in the stanza.

We should also work out how we want this to interact with dune coq top. I am not sure we are going to be able to interactively build plugins when they are loaded and these declare statements will have to live in existing .v files. This could be annoying.

It should still be possible for users to declare a plugins field however and we have to work out if this should override or complement the inferred plugins.

Start by tracing how the coq.theory stanza handles its plugins field and how dune coq top loads plugins. Determine how Declare ML Module entries in .v files should be discovered for Coq 8.16 and newer while preserving current behavior for older versions. Resolve whether explicit plugins complement or override inferred ones, and account for the dependency limitation described in issue #7893.