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.

9 files changed, 52 insertions, 52 deletions

diff --git a/CHANGES b/CHANGES
index 5a63df21f7..48b39a01fb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,10 @@ Vernacular commands
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
+- The coq/user-contrib directory and the XDG directories are no longer
+  recursively added to the load path, so files from installed libraries
+  now need   to be fully qualified for the "Require" command to find
+  them. The tools/update-require script can be used to convert a development.
 
 Notations
 
@@ -68,7 +72,7 @@ Tactics
   independently of the number of ipats, which has itself to be less
   than the number of new hypotheses (possible source of incompatibilities;
   former behavior obtainable by "Unset Injection L2R Pattern Order").
-- New tactic "rewrite_strat" for generalized rewriting with user-defined 
+- New tactic "rewrite_strat" for generalized rewriting with user-defined
   strategies, subsumming autorewrite.
 
 Program
@@ -89,6 +93,16 @@ Notations
 - More systematic insertion of spaces as a default for printing
   notations ("format" still available to override the default).
 
+Tools
+
+- Option -I now only adds directories to the ml path. To add to both
+  the load path and the ml path, use -I -as.
+- Option -R no longer adds recursively to the ml path; only the root
+  directory is added. (Behavior with respect to the load path is
+  unchanged.)
+- Option -nois prevents coq/theories and coq/plugins to be recursively
+  added to the load path. (Same behavior as with coq/user-contrib.)
+
 Internal Infrastructure
 
 - Many reorganisations in the ocaml source files. For instance,
@@ -109,7 +123,7 @@ Internal Infrastructure
   * The -coqrunbyteflags and its blank-separated argument is replaced
     by option -vmbyteflags which expects a comma-separated argument.
   * The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
- 
+
 Changes from V8.4beta2 to V8.4
 ==============================
 
diff --git a/Makefile.build b/Makefile.build
index c79b21f407..2d942d1fb2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -471,7 +471,7 @@ pluginsbyte: $(PLUGINS)
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
 	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit
+	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
diff --git a/lib/flags.ml b/lib/flags.ml
index 3118901ac5..9b932946ca 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -42,7 +42,7 @@ let with_extra_values o l f x =
     raise reraise
 
 let boot = ref false
-
+let load_init = ref true
 let batch_mode = ref false
 
 type compilation_mode = BuildVo | BuildVi | Vi2Vo
diff --git a/lib/flags.mli b/lib/flags.mli
index 6c6aa5fbeb..ebd11ee774 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -9,6 +9,7 @@
 (** Global options of the system. *)
 
 val boot : bool ref
+val load_init : bool ref
 
 val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVi | Vi2Vo
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\