Change handling of loadpath and mlpath.

- Option -I no longer handles loadpath, only mlpath. This is the same
  behavior as coq_makefile. Option -I-as is unchanged.
- Option -R no longer recursively adds to mlpath; only the root directory
  is added.
- user-contrib/ and xdg directories are no longer recursively added to
  the loadpath.
- theories/ and plugins/ are no longer recursively added to the loadpath
  when option -nois is passed.
- All the preconfigured directories are still recursively added to the
  mlpath though.

5 files changed, 33 insertions, 48 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f9c9b009aa..005f6c4ec7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,41 +59,28 @@ let load_rcfile() =
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s])
-let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root])
+  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]);
+  Mltop.add_ml_dir unix_path
 
-(* By the option -include -I or -R of the command line *)
+(* Recursively puts dir in the LoadPath if -nois was not passed *)
+let add_stdlib_path ~unix_path ~coq_root ~with_ml =
+  if !Flags.load_init then
+    Mltop.add_rec_path ~unix_path ~coq_root
+  else
+    Mltop.add_path ~unix_path ~coq_root;
+  if with_ml then
+    Mltop.add_rec_ml_dir unix_path
+
+let add_userlib_path ~unix_path =
+  Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix;
+  Mltop.add_rec_ml_dir unix_path
+
+(* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
-
-(* The list of all theories in the standard library /!\ order does matter *)
-let theories_dirs_map = [
-    "theories/Unicode", "Unicode" ;
-    "theories/Classes", "Classes" ;
-    "theories/Program", "Program" ;
-    "theories/MSets", "MSets" ;
-    "theories/FSets", "FSets" ;
-    "theories/Reals", "Reals" ;
-    "theories/Strings", "Strings" ;
-    "theories/Sorting", "Sorting" ;
-    "theories/Setoids", "Setoids" ;
-    "theories/Sets", "Sets" ;
-    "theories/Structures", "Structures" ;
-    "theories/Lists", "Lists" ;
-    "theories/Vectors", "Vectors" ;
-    "theories/Wellfounded", "Wellfounded" ;
-    "theories/Relations", "Relations" ;
-    "theories/Numbers", "Numbers" ;
-    "theories/QArith", "QArith" ;
-    "theories/PArith", "PArith" ;
-    "theories/NArith", "NArith" ;
-    "theories/ZArith", "ZArith" ;
-    "theories/Arith", "Arith" ;
-    "theories/Bool", "Bool" ;
-    "theories/Logic", "Logic" ;
-    "theories/Init", "Init"
-  ]
+let ml_includes = ref []
+let push_ml_include s = ml_includes := s :: !ml_includes
 
 (* Initializes the LoadPath *)
 let init_load_path () =
@@ -101,30 +88,30 @@ let init_load_path () =
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
-  let dirs = ["plugins"] in
+  let coq_root = Names.DirPath.make [Nameops.coq_root] in
     (* NOTE: These directories are searched from last to first *)
     (* first, developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
-    List.iter
-      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.DirPath.make [Names.Id.of_string alias; Nameops.coq_root]))
-      theories_dirs_map;
+    add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
-    List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
+    add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
     (* then user-contrib *)
     if Sys.file_exists user_contrib then
-      Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix;
+      add_userlib_path ~unix_path:user_contrib;
     (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
-    List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) xdg_dirs;
+    List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs;
     (* then directories in COQPATH *)
-    List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) coqpath;
+    List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
     (* then current directory *)
     Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix;
-    (* additional loadpath, given with -I -include -R options *)
+    (* additional loadpath, given with options -I-as and -R *)
     List.iter
       (fun (unix_path, coq_root, reci) ->
 	if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root)
-      (List.rev !includes)
+      (List.rev !includes);
+    (* additional ml directories, given with option -I *)
+    List.iter Mltop.add_ml_dir (List.rev !ml_includes)
 
 let init_library_roots () =
   includes := []
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 88b7a9e9d1..4ca8b61f8c 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -17,6 +17,7 @@ val load_rcfile : unit -> unit
 
 val push_include : string * Names.DirPath.t -> unit
 val push_rec_include : string * Names.DirPath.t -> unit
+val push_ml_include : string -> unit
 
 val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d2f680d6e3..6d92eaa5a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -99,8 +99,6 @@ let load_vernac_obj () =
   List.iter (fun f -> Library.require_library_from_file None f None)
     (List.rev !load_vernacular_obj)
 
-let load_init = ref true
-
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
   Library.require_library_from_dirpath [Coqlib.prelude_module,vo] (Some true)
@@ -309,7 +307,7 @@ let parse_args arglist =
       begin match rem with
       | d :: "-as" :: p :: rem -> set_include d p; args := rem
       | d :: "-as" :: [] -> error_missing_arg "-as"
-      | d :: rem -> set_default_include d; args := rem
+      | d :: rem -> push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
     |"-R" ->
@@ -319,7 +317,7 @@ let parse_args arglist =
       | d :: p :: rem -> set_rec_include d p; args := rem
       | _ -> error_missing_arg opt
       end
-    
+
     (* Options with two arg *)
     |"-check-vi-tasks" ->
         let tno = get_task_list (next ()) in
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index e0cb2209d5..cc9aa59aa4 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -178,7 +178,6 @@ let add_rec_path ~unix_path ~coq_root =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
-    let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in
     let () = add_ml_dir unix_path in
     let add (path, dir) = Loadpath.add_load_path path false dir in
     let () = List.iter add dirs in
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8d5aebc700..8343140948 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -18,9 +18,9 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "Coq options are:\n";
   output_string co
-"  -I dir -as coqdir      map physical dir to logical coqdir\
-\n  -I dir                 map directory dir to the empty logical path\
+"  -I dir                 look for ML files in dir\
 \n  -include dir           (idem)\
+\n  -I dir -as coqdir      map physical dir to logical coqdir\
 \n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
 \n  -R dir coqdir          (idem)\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\