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.

1 files changed, 16 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 5a63df21f..48b39a01f 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
 ==============================