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 .
---
 stm/stm.ml  | 4 ++--
 stm/stm.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 6f7cefb582..2a7fb084fc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2661,7 +2661,7 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Mltop.coq_path list;
+  iload_path   : Loadpath.coq_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
@@ -2719,7 +2719,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   (* Set load path; important, this has to happen before we declare
      the library below as [Declaremods/Library] will infer the module
      name by looking at the load path! *)
-  List.iter Mltop.add_coq_path iload_path;
+  List.iter Loadpath.add_coq_path iload_path;
 
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 9d2bf56629..73f3ffab7e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -69,7 +69,7 @@ type stm_init_options = {
 
   (* Initial load path in scope for the document. Usually extracted
      from -R options / _CoqProject *)
-  iload_path   : Mltop.coq_path list;
+  iload_path   : Loadpath.coq_path list;
 
   (* Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
-- 
cgit v1.2.3