Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to vernac

Reviewed-by: maximedenes

6 files changed, 20 insertions, 20 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 2f63410761..7748134146 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -225,7 +225,7 @@ let do_vio opts copts =
      process happens outside of the STM *)
   if copts.vio_files <> [] || copts.vio_tasks <> [] then
     let iload_path = build_load_path opts in
-    List.iter Mltop.add_coq_path iload_path;
+    List.iter Loadpath.add_coq_path iload_path;
 
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index ec43dbb1d7..4ef31c73b7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -46,8 +46,8 @@ type t = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : Mltop.coq_path list;
-  vo_includes : Mltop.coq_path list;
+  ml_includes : Loadpath.coq_path list;
+  vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -147,10 +147,10 @@ let default = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
+  Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes }
 
 let add_vo_include opts unix_path coq_path implicit =
-  let open Mltop in
+  let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
   { opts with vo_includes = {
         recursive = true;
@@ -273,7 +273,7 @@ let usage help =
   end;
   let lp = Coqinit.toplevel_init_load_path () in
   (* Necessary for finding the toplevels below *)
-  List.iter Mltop.add_coq_path lp;
+  List.iter Loadpath.add_coq_path lp;
   help ()
 
 (* Main parsing routine *)
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index d7f9819bee..015789c1f3 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -22,8 +22,8 @@ type t = {
   load_rcfile : bool;
   rcfile      : string option;
 
-  ml_includes : Mltop.coq_path list;
-  vo_includes : Mltop.coq_path list;
+  ml_includes : Loadpath.coq_path list;
+  vo_includes : Loadpath.coq_path list;
   vo_requires : (string * string option * bool option) list;
 
   toplevel_name : Stm.interactive_top;
@@ -69,4 +69,4 @@ val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list
 val exitcode : t -> int
 
 val require_libs : t -> (string * string option * bool option) list
-val build_load_path : t -> Mltop.coq_path list
+val build_load_path : t -> Loadpath.coq_path list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 74a089510e..cbe353004e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -53,25 +53,25 @@ let load_rcfile ~rcfile ~state =
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
-  let open Mltop in
+  let open Loadpath in
   let add_ml = if with_ml then AddRecML else AddNoML in
   { recursive = true;
     path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init }
   }
 
 let build_userlib_path ~unix_path =
-  let open Mltop in
+  let open Loadpath in
   { recursive = true;
     path_spec = VoPath {
         unix_path;
         coq_path = Libnames.default_root_prefix;
-        has_ml = Mltop.AddRecML;
+        has_ml = AddRecML;
         implicit = false;
       }
   }
 
 let ml_path_if c p =
-  let open Mltop in
+  let open Loadpath in
   let f x = { recursive = false; path_spec = MlPath x } in
   if c then List.map f p else []
 
@@ -85,7 +85,7 @@ let toplevel_init_load_path () =
 (* LoadPath for Coq user libraries *)
 let libs_init_load_path ~load_init =
 
-  let open Mltop in
+  let open Loadpath in
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
@@ -115,10 +115,10 @@ let libs_init_load_path ~load_init =
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
-  let open Mltop in
+  let open Loadpath in
   let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
+    Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
   in
-    Mltop.add_coq_path (lp (Envars.coqlib ()));
+    Loadpath.add_coq_path (lp (Envars.coqlib ()));
     List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index c891e736b4..04ec77a025 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State
 val init_ocaml_path : unit -> unit
 
 (* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Mltop.coq_path list
+val toplevel_init_load_path : unit -> Loadpath.coq_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : load_init:bool -> Mltop.coq_path list
+val libs_init_load_path : load_init:bool -> Loadpath.coq_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b769405cf6..460c2f126e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -222,7 +222,7 @@ let init_toplevel ~help ~init custom_init arglist =
     exit 0;
   end;
   let top_lp = Coqinit.toplevel_init_load_path () in
-  List.iter Mltop.add_coq_path top_lp;
+  List.iter Loadpath.add_coq_path top_lp;
   let opts, extras = custom_init ~opts extras in
   Mltop.init_known_plugins ();