[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 .

1 files changed, 3 insertions, 21 deletions

diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 3d796aa4aa..b457c9c88f 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -32,6 +32,9 @@ val ocaml_toploop : unit -> unit
 
 (** {5 ML Dynlink} *)
 
+(** Adds a dir to the plugin search path *)
+val add_ml_dir : recursive:bool -> string -> unit
+
 (** Tests if we can load ML files *)
 val has_dynlink : bool
 
@@ -41,27 +44,6 @@ val dir_ml_load : string -> unit
 (** Dynamic interpretation of .ml *)
 val dir_ml_use : string -> unit
 
-(** Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
-  unix_path : string;           (* Filesystem path contaning vo/ml files *)
-  coq_path  : Names.DirPath.t;  (* Coq prefix for the path *)
-  implicit  : bool;             (* [implicit = true] avoids having to qualify with [coq_path] *)
-  has_ml    : add_ml;           (* If [has_ml] is true, the directory will also be search for plugins *)
-}
-
-type coq_path_spec =
-  | VoPath of vo_path_spec
-  | MlPath of string
-
-type coq_path = {
-  path_spec: coq_path_spec;
-  recursive: bool;
-}
-
-val add_coq_path : coq_path -> unit
-
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
 val module_is_known : string -> bool