[toplevel] Refactor load path handling.

We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.

To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:

```
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;
}
```

Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.

This API is necessarily internal [for now] thus I don't think a
changes entry is needed.

1 files changed, 5 insertions, 2 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3358951f4..1a02a22a5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -905,9 +905,11 @@ let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
 let vernac_add_loadpath implicit pdir ldiropt =
+  let open Mltop in
   let pdir = expand pdir in
   let alias = Option.default Libnames.default_root_prefix ldiropt in
-  Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
+  add_coq_path { recursive = true;
+                 path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
@@ -915,7 +917,8 @@ let vernac_remove_loadpath path =
   (* Coq syntax for ML or system commands *)
 
 let vernac_add_ml_path isrec path =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path)
+  let open Mltop in
+  add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
 
 let vernac_declare_ml_module ~atts l =
   let local = make_locality atts.locality in