From eb15c59bb2f79f0154a0c37e43cdf4e90235c053 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 8 Apr 2014 20:01:41 +0200
Subject: Add an option -Q (tentative name).

This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.
---
 CHANGES | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ceabc053dc..7cd2c24990 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,8 +15,8 @@ Vernacular commands
   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.
+  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
 
@@ -97,8 +97,10 @@ 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 -nois prevents coq/theories and coq/plugins to be recursively
-  added to the load path. (Same behavior as with coq/user-contrib.)
+- Option -Q behaves as -I -as and -R, except that the logical path of
+  any loaded file has to be fully qualified.
+- Option -nois loads coq/theories and coq/plugins as if using -Q rather
+  than -R. (Same behavior as with coq/user-contrib.)
 
 Internal Infrastructure
 
-- 
cgit v1.2.3