From 8b2505b5526395d2ad3c5126624a070e0f55a8af Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 17:04:30 +0200
Subject: [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 .
---
 vernac/vernac.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/vernac.mllib')

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
-- 
cgit v1.2.3