diff options
| author | Emilio Jesus Gallego Arias | 2019-04-02 17:04:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 20:17:27 +0200 |
| commit | 8b2505b5526395d2ad3c5126624a070e0f55a8af (patch) | |
| tree | 3c434c37564f09a88aaa5de8dd0b5880204a5b50 /vernac/vernac.mllib | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
[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 .
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7f5c265eea..57c56a58f9 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ Assumptions Vernacstate Mltop Topfmt +Loadpath Vernacentries Misctypes |