[coq] Reify legacy lib resolution

We redo the legacy / installed lib resolution as to happen in two
stages, as discussed; note that this is not really necessary (yet) as
the semantics for resolution of installed legacy libs don't require
access to the library / theory database.

This will change when we detect Coq theories installed / created by
Dune.

Missing tests:

- native with installed theories, with transitive deps
- older Coq (8.13?)
- plugin in installed subdirs / coqpath without findlib registration
- behavior of subtheories A.B.C vs A.B vs A

Changes wrt main:

- `requires_for_user_written` was buggy in the sense that
  it didn't resolve the current theory. This is a
  delicate point as resolution is required for example to maybe add
  the boot lib, so in extraction we must do that.

- I have unlined some code that should not have been inlined, also
  refactored away quite a bit of duplication due to `dune coq top`

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

CHANGES.md

@@ -29,7 +29,7 @@ Unreleased
 
 - Dune can now detect Coq theories from outside the workspace. This allows for
   composition with installed theories (not necessarily installed with Dune).
-  (#7047, @Alizter)
+  (#7047, @Alizter, @ejgallego)
 
 - `dune coq top` now correctly respects the project root when called from a
   subdirectory. However, absolute filenames passed to `dune coq top` are no