[loadpath] Make loadpath handling self-contained and move to vernac

We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]

This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.

Logic could be pushed upwards, but this is good enough for now.

This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.

The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .

0 files changed, 0 insertions, 0 deletions