Make it explicit when paths are added to the ML search paths.

When Mltop.add_rec_path was called to add paths to the loadpath, it was
also adding the top directory to the mlpath. In particular, "theories" was
added to the mlpath although it was explicitly marked "~with_ml:false".

The "plugins" and "user-contribs" subdirectories were scanned twice, once
for filling the loadpath and then for filling the mlpath.

This patch adds an argument to Mltop.add_rec_path to explicitly control
which paths from the loadpath are added to the mlpath (none, the top one,
all of them). The "top" option was the single old behavior; the "none"
option is used for "theories"; the "all" option is used to avoid
duplicate scanning for "plugins" and "user-contribs".

4 files changed, 16 insertions, 10 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d9cd574a04..258a1135fc 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,13 +59,12 @@ let load_rcfile() =
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
-  Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init);
-  if with_ml then
-    Mltop.add_rec_ml_dir unix_path
+  let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
+  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init)
 
 let add_userlib_path ~unix_path =
-  Mltop.add_rec_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
-  Mltop.add_rec_ml_dir unix_path
+  Mltop.add_rec_path Mltop.AddRecML ~unix_path
+    ~coq_root:Nameops.default_root_prefix ~implicit:false
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
@@ -108,7 +107,7 @@ let init_load_path () =
     (* additional loadpath, given with options -Q and -R *)
     List.iter
       (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path ~unix_path ~coq_root ~implicit)
+        Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index f972959453..0a5b92270f 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -182,7 +182,9 @@ let warn_cannot_open_path =
   CWarnings.create ~name:"cannot-open-path" ~category:"filesystem"
       (fun unix_path -> str "Cannot open " ++ str unix_path)
 
-let add_rec_path ~unix_path ~coq_root ~implicit =
+type add_ml = AddNoML | AddTopML | AddRecML
+
+let add_rec_path add_ml ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = Names.DirPath.repr coq_root in
@@ -193,7 +195,10 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = add_ml_dir unix_path in
+    let () = match add_ml with
+      | AddNoML -> ()
+      | AddTopML -> add_ml_dir unix_path
+      | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
     let add (path, dir) =
       Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 5d05468241..6633cb9372 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -46,8 +46,10 @@ val dir_ml_use : string -> unit
 val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
+type add_ml = AddNoML | AddTopML | AddRecML
+
 (** Adds a path to the Coq and ML paths *)
-val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
+val add_rec_path : add_ml -> unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33a8609a77..48a85b709f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -880,7 +880,7 @@ let expand filename =
 let vernac_add_loadpath implicit pdir ldiropt =
   let pdir = expand pdir in
   let alias = Option.default Nameops.default_root_prefix ldiropt in
-  Mltop.add_rec_path ~unix_path:pdir ~coq_root:alias ~implicit
+  Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)