Merge PR #11618: [loadpath] Rework and simplify ML loadpath handling

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes

22 files changed, 157 insertions, 215 deletions

diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst
new file mode 100644
index 0000000000..77fa556321
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  Recursive OCaml loadpaths are not supported anymore; the command
+  ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the
+  preferred one. We have also dropped support for the non-qualified
+  version of the :cmd:`Add LoadPath` command, that is to say,
+  the ``Add LoadPath dir`` version; now,
+  you must always specify a prefix now using ``Add Loadpath dir as Prefix.``
+  (`#11618 <https://github.com/coq/coq/pull/11618>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a38c26c2b3..d1f3dcc309 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged.
    :n:`-Q @string @dirpath`. It adds the physical directory string to the current
    |Coq| loadpath and maps it to the logical directory dirpath.
 
-   .. cmdv:: Add LoadPath @string
-
-      Performs as :n:`Add LoadPath @string @dirpath` but
-      for the empty directory path.
-
 
 .. cmd:: Add Rec LoadPath @string as @dirpath
 
@@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged.
    :n:`-R @string @dirpath`. It adds the physical directory string and all its
    subdirectories to the current |Coq| loadpath.
 
-   .. cmdv:: Add Rec LoadPath @string
-
-      Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty
-      logical directory path.
-
 
 .. cmd:: Remove LoadPath @string
 
@@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged.
    loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
-.. cmd:: Add Rec ML Path @string
-
-   This command adds the directory :n:`@string` and all its subdirectories to
-   the current OCaml loadpath (see the command :cmd:`Declare ML Module`).
-
-
 .. cmd:: Print ML Path @string
 
    This command displays the current OCaml loadpath. This
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 5b9ea17ba7..790b427e4c 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -21,7 +21,6 @@ let commands = [
    "Add Printing Let";
    "Add Printing Record";
    "Add Rec LoadPath";
-   "Add Rec ML Path";
    "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
    "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].";
    "Add Relation";
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml
index dfc16d39f3..4292e91252 100644
--- a/ide/fake_ide.ml
+++ b/ide/fake_ide.ml
@@ -327,11 +327,7 @@ let main =
     { xml_printer = op; xml_parser = ip } in
   let init () =
     match base_eval_call ~print:false (Xmlprotocol.init None) coq with
-    | Interface.Good id ->
-        let dir = Filename.dirname input_file in
-        let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in
-        let eid, tip = add_sentence ~name:"initial" phrase in
-        after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq)
+    | Interface.Good id -> ()
     | Interface.Fail _ -> error "init call failed" in
   let finish () =
     match base_eval_call (Xmlprotocol.status true) coq with
diff --git a/stm/stm.ml b/stm/stm.ml
index 95c58b9043..109ac2d8b4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2569,28 +2569,32 @@ end (* }}} *)
 (********************************* STM API ************************************)
 (******************************************************************************)
 
-(* Main initialization routine *)
-type stm_init_options = {
-  (* The STM will set some internal flags differently depending on the
-     specified [doc_type]. This distinction should disappear at some
-     some point. *)
-  doc_type     : stm_doc_type;
-
-  (* Initial load path in scope for the document. Usually extracted
-     from -R options / _CoqProject *)
-  iload_path   : Loadpath.coq_path list;
-
-  (* Require [require_libs] before the initial state is
+(** STM initialization options: *)
+type stm_init_options =
+  { doc_type : stm_doc_type
+  (** The STM does set some internal flags differently depending on
+     the specified [doc_type]. This distinction should disappear at
+     some some point. *)
+
+  ; ml_load_path : CUnix.physical_path list
+  (** OCaml load paths for the document. *)
+
+  ; vo_load_path   : Loadpath.vo_path list
+  (** [vo] load paths for the document. Usually extracted from -R
+     options / _CoqProject *)
+
+  ; require_libs : (string * string option * bool option) list
+  (** Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
      [lib,prefix,import_export] means require library [lib] from
      optional [prefix] and [import_export] if [Some false/Some true]
      is used.  *)
-  require_libs : (string * string option * bool option) list;
 
-  (* STM options that apply to the current document. *)
-  stm_options  : AsyncOpts.stm_opt;
-}
-(* fb_handler   : Feedback.feedback -> unit; *)
+  ; stm_options  : AsyncOpts.stm_opt
+  (** Low-level STM options *)
+  }
+
+  (* fb_handler   : Feedback.feedback -> unit; *)
 
 (*
 let doc_type_module_name (std : stm_doc_type) =
@@ -2615,7 +2619,7 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; iload_path; require_libs; stm_options } =
+let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } =
 
   let require_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
@@ -2633,7 +2637,8 @@ 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 Loadpath.add_coq_path iload_path;
+  List.iter Mltop.add_ml_dir ml_load_path;
+  List.iter Loadpath.add_vo_path vo_load_path;
 
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 841adcf05b..e56bac6e0f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,38 +52,30 @@ type stm_doc_type =
   | VioDoc      of string       (* file path *)
   | Interactive of interactive_top    (* module path *)
 
-(** Coq initialization options:
-
- - [doc_type]: Type of document being created.
-
- - [require_libs]: list of libraries/modules to be pre-loaded at
-   startup. A tuple [(modname,modfrom,import)] is equivalent to [From
-   modfrom Require modname]; [import] works similarly to
-   [Library.require_library_from_dirpath], [Some false] will import
-   the module, [Some true] will additionally export it.
-
-*)
-type stm_init_options = {
-  (* The STM will set some internal flags differently depending on the
-     specified [doc_type]. This distinction should disappear at some
-     some point. *)
-  doc_type     : stm_doc_type;
-
-  (* Initial load path in scope for the document. Usually extracted
-     from -R options / _CoqProject *)
-  iload_path   : Loadpath.coq_path list;
-
-  (* Require [require_libs] before the initial state is
+(** STM initialization options: *)
+type stm_init_options =
+  { doc_type : stm_doc_type
+  (** The STM does set some internal flags differently depending on
+     the specified [doc_type]. This distinction should disappear at
+     some some point. *)
+
+  ; ml_load_path : CUnix.physical_path list
+  (** OCaml load paths for the document. *)
+
+  ; vo_load_path   : Loadpath.vo_path list
+  (** [vo] load paths for the document. Usually extracted from -R
+     options / _CoqProject *)
+
+  ; require_libs : (string * string option * bool option) list
+  (** Require [require_libs] before the initial state is
      ready. Parameters follow [Library], that is to say,
      [lib,prefix,import_export] means require library [lib] from
      optional [prefix] and [import_export] if [Some false/Some true]
      is used.  *)
-  require_libs : (string * string option * bool option) list;
 
-  (* STM options that apply to the current document. *)
-  stm_options  : AsyncOpts.stm_opt;
-}
-(* fb_handler   : Feedback.feedback -> unit; *)
+  ; stm_options  : AsyncOpts.stm_opt
+  (** Low-level STM options *)
+  }
 
 (** The type of a STM document *)
 type doc
diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake
index aa68fad39e..38c610a5a6 100644
--- a/test-suite/ide/debug_ltac.fake
+++ b/test-suite/ide/debug_ltac.fake
@@ -1,2 +1,3 @@
+ADD { Comments "fakeide doesn't support fail as the first sentence". }
 FAILADD { Debug On. }
 ADD { Set Debug On. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index 5284c5d3a5..eb553f9dfa 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,6 +3,7 @@
 #
 # Simple backtrack by 2 before two global definitions
 #
+ADD initial { Comments "initial sentence". }
 ADD { Definition foo := 0. }
 ADD { Definition bar := 1. }
 EDIT_AT initial
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index dceb811d66..f75a706041 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -104,7 +104,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
@@ -129,8 +129,8 @@ let compile opts copts ~echo ~f_in ~f_out =
   | BuildVo | BuildVok ->
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VoDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
@@ -181,8 +181,8 @@ let compile opts copts ~echo ~f_in ~f_out =
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
-          Stm.{ doc_type = VioDoc long_f_dot_out;
-                iload_path; require_libs; stm_options;
+          Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
+                vo_load_path; require_libs; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
@@ -252,8 +252,9 @@ let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling
      process happens outside of the STM *)
   if copts.vio_files <> [] || copts.vio_tasks <> [] then
-    let iload_path = build_load_path opts in
-    List.iter Loadpath.add_coq_path iload_path;
+    let ml_lp, vo_lp = build_load_path opts in
+    List.iter Mltop.add_ml_dir ml_lp;
+    List.iter Loadpath.add_vo_path vo_lp;
 
   (* Vio compile pass *)
   if copts.vio_files <> [] then schedule_vio copts;
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 949a13974c..24cfecd057 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -70,8 +70,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : string list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -164,14 +164,13 @@ let default = {
 (* Functional arguments                                                       *)
 (******************************************************************************)
 let add_ml_include opts s =
-  Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }}
+  { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
 
 let add_vo_include opts unix_path coq_path implicit =
   let open Loadpath in
   let coq_path = Libnames.dirpath_of_string coq_path in
   { opts with pre = { opts.pre with vo_includes = {
-        recursive = true;
-        path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }}
+        unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
   { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
@@ -582,9 +581,7 @@ let prelude_data = "Prelude", Some "Coq", Some false
 let require_libs opts =
   if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
 
-let cmdline_load_path opts =
-  opts.pre.ml_includes @ opts.pre.vo_includes
-
 let build_load_path opts =
-  (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @
-  cmdline_load_path opts
+  let ml_path, vo_path = if opts.pre.boot then [],[] else Coqinit.libs_init_load_path () in
+  ml_path @ opts.pre.ml_includes ,
+  vo_path @ opts.pre.vo_includes
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index aba6811f43..88de48967a 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -46,8 +46,8 @@ type coqargs_pre = {
   load_init   : bool;
   load_rcfile : bool;
 
-  ml_includes : Loadpath.coq_path list;
-  vo_includes : Loadpath.coq_path list;
+  ml_includes : CUnix.physical_path list;
+  vo_includes : Loadpath.vo_path list;
   vo_requires : (string * string option * bool option) list;
   (* None = No Import; Some false = Import; Some true = Export *)
 
@@ -83,4 +83,4 @@ val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * strin
 val error_wrong_arg : string -> unit
 
 val require_libs : t -> (string * string option * bool option) list
-val build_load_path : t -> Loadpath.coq_path list
+val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7f3d4b570f..ce054d2af2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,34 +51,22 @@ let load_rcfile ~rcfile ~state =
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
       iraise reraise
 
-(* Recursively puts `.v` files in the LoadPath if -nois was not passed *)
+(* Recursively puts `.v` files in the LoadPath *)
 let build_stdlib_vo_path ~unix_path ~coq_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true }
-  }
-
-let build_stdlib_ml_path ~dir =
-  let open Loadpath in
-  { recursive = true
-  ; path_spec = MlPath dir
-  }
+  { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true }
 
 let build_userlib_path ~unix_path =
   let open Loadpath in
-  { recursive = true;
-    path_spec = VoPath {
-        unix_path;
-        coq_path = Libnames.default_root_prefix;
-        has_ml = AddRecML;
-        implicit = false;
-      }
+  { unix_path
+  ; coq_path = Libnames.default_root_prefix
+  ; has_ml = true
+  ; implicit = false
+  ; recursive = true
   }
 
 let ml_path_if c p =
-  let open Loadpath in
-  let f x = { recursive = false; path_spec = MlPath x } in
-  if c then List.map f p else []
+  if c then p else []
 
 (* LoadPath for developers *)
 let toplevel_init_load_path () =
@@ -97,16 +85,19 @@ let libs_init_load_path () =
   let coqpath = Envars.coqpath in
   let coq_path = Names.DirPath.make [Libnames.coq_root] in
 
+  (* ML includes *)
+  let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in
+  List.map fst plugins_dirs,
+
   (* current directory (not recursively!) *)
-  [ { recursive = false;
-      path_spec = VoPath { unix_path = ".";
-                           coq_path = Libnames.default_root_prefix;
-                           implicit = false;
-                           has_ml = AddTopML }
+  [ { unix_path = "."
+    ; coq_path = Libnames.default_root_prefix
+    ; implicit = false
+    ; has_ml = true
+    ; recursive = false
     } ] @
 
   (* then standard library *)
-  [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @
   [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @
 
   (* then user-contrib *)
@@ -120,10 +111,8 @@ let libs_init_load_path () =
 (* 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 Loadpath in
-  let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl]))
+    Mltop.add_ml_dir (List.fold_left (/) (Envars.coqlib()) [dl])
   in
-    Loadpath.add_coq_path (lp (Envars.coqlib ()));
-    List.iter add_subdir Coq_config.all_src_dirs
+  Mltop.add_ml_dir (Envars.coqlib ());
+  List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index f3a007d987..f099173808 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 -> Loadpath.coq_path list
+val toplevel_init_load_path : unit -> CUnix.physical_path list
 
 (* LoadPath for Coq user libraries *)
-val libs_init_load_path : unit -> Loadpath.coq_path list
+val libs_init_load_path : unit -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1ea48ee766..1e6b1023fe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -226,7 +226,7 @@ let init_execution opts custom_init =
   Spawned.init_channels ();
   if opts.post.memory_stat then at_exit print_memory_stat;
   let top_lp = Coqinit.toplevel_init_load_path () in
-  List.iter Loadpath.add_coq_path top_lp;
+  List.iter Mltop.add_ml_dir top_lp;
   CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority);
   Mltop.init_known_plugins ();
   (* Configuration *)
@@ -281,14 +281,14 @@ let init_document opts =
   *)
   (* Next line allows loading .vos files when in interactive mode *)
   Flags.load_vos_libraries := true;
-  let iload_path = build_load_path opts in
+  let ml_load_path, vo_load_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             iload_path; require_libs; stm_options;
+             ml_load_path; vo_load_path; require_libs; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 8486de3aed..37b584f8d9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -912,10 +912,11 @@ GRAMMAR EXTEND Gram
       | IDENT "Locate"; l = locatable -> { VernacLocate l }
 
       (* Managing load paths *)
-      | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
-          { VernacAddLoadPath (false, dir, alias) }
-      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string;
-          alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) }
+      | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+          { VernacAddLoadPath { implicit = false; logical_path; physical_path } }
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath ->
+          { VernacAddLoadPath { implicit = true; logical_path; physical_path } }
+
       | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
           { VernacRemoveLoadPath dir }
 
@@ -934,9 +935,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) }
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-          { VernacAddMLPath (false, dir) }
-      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
-          { VernacAddMLPath (true, dir) }
+          { VernacAddMLPath dir }
 
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_setting ->
@@ -1070,9 +1069,6 @@ GRAMMAR EXTEND Gram
   option_table:
     [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
   ;
-  as_dirpath:
-    [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ]
-  ;
   ne_in_or_out_modules:
     [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
       | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 506b3bc505..38aa42c349 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -218,24 +218,18 @@ let try_locate_absolute_library dir =
 
 (** { 5 Extending the load path } *)
 
-(* Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
-  unix_path : string;  (* Filesystem path containing vo/ml files *)
-  coq_path  : DP.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;
-}
+type vo_path =
+  { unix_path : string
+  (** Filesystem path containing vo/ml files *)
+  ; coq_path  : DP.t
+  (** Coq prefix for the path *)
+  ; implicit  : bool
+  (** [implicit = true] avoids having to qualify with [coq_path] *)
+  ; has_ml    : bool
+  (** If [has_ml] is true, the directory will also be added to the ml include path *)
+  ; recursive : bool
+  (** [recursive] will determine whether we explore sub-directories  *)
+  }
 
 let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
@@ -255,9 +249,10 @@ let convert_string d =
     warn_cannot_use_directory d;
     raise Exit
 
-let add_vo_path ~recursive lp =
+let add_vo_path lp =
   let unix_path = lp.unix_path in
   let implicit = lp.implicit in
+  let recursive = lp.recursive in
   if System.exists_dir unix_path then
     let dirs = if recursive then System.all_subdirs ~unix_path else [] in
     let prefix = DP.repr lp.coq_path in
@@ -268,22 +263,17 @@ let add_vo_path ~recursive lp =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let add_ml_dir = Mltop.add_ml_dir ~recursive:false in
-    let () = match lp.has_ml with
-      | AddNoML -> ()
-      | AddTopML ->
-        Mltop.add_ml_dir ~recursive:false unix_path
-      | AddRecML ->
-        List.iter (fun (lp,_) -> add_ml_dir lp) dirs;
-        add_ml_dir unix_path in
+    let () =
+      if lp.has_ml && not lp.recursive then
+        Mltop.add_ml_dir unix_path
+      else if lp.has_ml && lp.recursive then
+        (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs;
+         Mltop.add_ml_dir unix_path)
+      else
+        ()
+    in
     let add (path, dir) = add_load_path path ~implicit dir in
     let () = List.iter add dirs in
     add_load_path unix_path ~implicit lp.coq_path
   else
     warn_cannot_open_path unix_path
-
-let add_coq_path { recursive; path_spec } = match path_spec with
-  | VoPath lp ->
-    add_vo_path ~recursive lp
-  | MlPath dir ->
-    Mltop.add_ml_dir ~recursive dir
diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli
index 47d2d34125..68212b9a47 100644
--- a/vernac/loadpath.mli
+++ b/vernac/loadpath.mli
@@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string
 (** {6 Extending the Load Path } *)
 
 (** Adds a path to the Coq and ML paths *)
-type add_ml = AddNoML | AddTopML | AddRecML
-
-type vo_path_spec = {
-  unix_path : string;
+type vo_path =
+  { unix_path : string
   (** Filesystem path containing vo/ml files *)
-  coq_path  : Names.DirPath.t;
+  ; coq_path  : DirPath.t
   (** Coq prefix for the path *)
-  implicit  : bool;
+  ; 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;
-}
+  ; has_ml    : bool
+  (** If [has_ml] is true, the directory will also be added to the ml include path *)
+  ; recursive : bool
+  (** [recursive] will determine whether we explore sub-directories  *)
+  }
 
-val add_coq_path : coq_path -> unit
+val add_vo_path : vo_path -> unit
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 5046248e11..671dae7876 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -128,11 +128,6 @@ let add_ml_dir s =
     | WithoutTop when has_dynlink -> keep_copy_mlpath s
     | _ -> ()
 
-(* For Rec Add ML Path (-R) *)
-let add_ml_dir ~recursive unix_path =
-  let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in
-  List.iter (fun (lp,_) -> add_ml_dir lp) dirs
-
 (* convertit un nom quelconque en nom de fichier ou de module *)
 let mod_of_name name =
     if Filename.check_suffix name ".cmo" then
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 271772d7ba..633a5c241d 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit
 (** {5 ML Dynlink} *)
 
 (** Adds a dir to the plugin search path *)
-val add_ml_dir : recursive:bool -> string -> unit
+val add_ml_dir : string -> unit
 
 (** Tests if we can load ML files *)
 val has_dynlink : bool
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 314c423f65..33d9e3d98a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1016,22 +1016,18 @@ let string_of_definition_object_kind = let open Decls in function
         return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
 
       (* Auxiliary file and library management *)
-      | VernacAddLoadPath (fl,s,d) ->
+      | VernacAddLoadPath { implicit; physical_path; logical_path } ->
         return (
           hov 2
             (keyword "Add" ++
-               (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++
-               keyword "LoadPath" ++ spc() ++ qs s ++
-               (match d with
-                 | None -> mt()
-                 | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir))
-        )
+             (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++
+             keyword "LoadPath" ++ spc() ++ qs physical_path ++
+             spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path))
       | VernacRemoveLoadPath s ->
         return (keyword "Remove LoadPath" ++ qs s)
-      | VernacAddMLPath (fl,s) ->
+      | VernacAddMLPath (s) ->
         return (
           keyword "Add"
-          ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc())
           ++ keyword "ML Path"
           ++ qs s
         )
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2eb1aa39b0..3cf4b4a89d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t =
 let expand filename =
   Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
 
-let vernac_add_loadpath implicit pdir ldiropt =
+let vernac_add_loadpath ~implicit pdir coq_path =
   let open Loadpath in
   let pdir = expand pdir in
-  let alias = Option.default Libnames.default_root_prefix ldiropt in
-  add_coq_path { recursive = true;
-                 path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } }
+  add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true }
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)
   (* Coq syntax for ML or system commands *)
 
-let vernac_add_ml_path isrec path =
-  let open Loadpath in
-  add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
+let vernac_add_ml_path path =
+  Mltop.add_ml_dir (expand path)
 
 let vernac_declare_ml_module ~local l =
   let local = Option.default false local in
@@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         unsupported_attributes atts;
         vernac_solve_existential ~pstate n c)
   (* Auxiliary file and library management *)
-  | VernacAddLoadPath (isrec,s,alias) ->
+  | VernacAddLoadPath { implicit; physical_path; logical_path } ->
     VtDefault(fun () ->
         unsupported_attributes atts;
-        vernac_add_loadpath isrec s alias)
+        vernac_add_loadpath ~implicit physical_path logical_path)
   | VernacRemoveLoadPath s ->
     VtDefault(fun () ->
         unsupported_attributes atts;
         vernac_remove_loadpath s)
-  | VernacAddMLPath (isrec,s) ->
+  | VernacAddMLPath (s) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
-        vernac_add_ml_path isrec s)
+        vernac_add_ml_path s)
   | VernacDeclareMLModule l ->
     VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
   | VernacChdir s ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 45018a246c..22aaab2a68 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -98,7 +98,6 @@ type search_restriction =
   | SearchInside of qualid list
   | SearchOutside of qualid list
 
-type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
@@ -363,9 +362,13 @@ type nonrec vernac_expr =
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
-  | VernacAddLoadPath of rec_flag * string * DirPath.t option
+  | VernacAddLoadPath of { implicit : bool
+                         ; physical_path : CUnix.physical_path
+                         ; logical_path : DirPath.t
+                         }
+
   | VernacRemoveLoadPath of string
-  | VernacAddMLPath of rec_flag * string
+  | VernacAddMLPath of string
   | VernacDeclareMLModule of string list
   | VernacChdir of string option