Review #2

Author: jfehrle

doc/sphinx/practical-tools/utilities.rst

@@ -269,8 +269,6 @@ locations such as `user-contrib` or `COQPATH` must either use an exact logical p
 or include a `From` clause (as if they are available through `-Q`).  This is done
 to reduce the number of ambiguous logical paths.
 
-.. todo I expect .vo files convert all logical paths into absolute paths.
-
 The mechanisms for creating logical paths for your multi-directory project are:
 
 - Through command line options passed on the command line to `coqc` and `coqide`,
@@ -284,9 +282,7 @@ The mechanisms for creating logical paths for your multi-directory project are:
   the other IDEs, they automatically look for a `_CoqProject` file in a
   parent directory of the script file, and, if found, they apply the parameters from
   `_CoqProject`.  Note that the `_CoqProject` file is ignored when Coq loads
-  compiled files from the package.  (Also, when loading, every `.vo` file under the
-  package directory is considered part of the package even if its `.v` file isn't
-  listed in the `_CoqProject`.)
+  compiled files from the package; every `.vo` file under the package directory is loaded.
 
   Coq tools are limited to using only one `_CoqProject` at a time, so multi-package
   projects need another mechanism.
@@ -337,12 +333,8 @@ Those added options shouldn't appear in published packages.
 .. todo I thought @herbelin added code to complain about ambiguous short names
    I made up some stuff below, need to check it:
 
-If you associate the same logical name with more than one directory, Coq will
-use the last one added (i.e., that appears earlier in :cmd:`Print LoadPath`).
-Nor will Coq complain if the short name of a package is ambiguous.  Perhaps
-in the future, Coq will be able to report such conflicts.  We recommend using
-the :n:`From @dirpath` option of :cmd:`Require` to make the behavior more predictable.
-
+If you associate the same logical name with more than one directory, Coq
+uses the last one added (i.e., that appears earlier in :cmd:`Print LoadPath`).
 
 Upgrading to a new version of Coq
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -547,8 +547,7 @@ file is a particular case of a module called a *library file*.
    reloaded. If :n:`Import` or :n:`Export` are present, the command also does
    the equivalent of the :cmd:`Import` or :cmd:`Export` commands.
 
-   Compiled files can sometimes be loaded using suffixes of the file's
-   fully qualified name.
+   A single file can be loaded with several variations of the `Require` command.
    For example, the ``-Q path Lib`` command line parameter associates the file
    ``path/Foo/File.vo`` with the logical name ``Lib.Foo.File``.  It allows this
    file to be loaded through :n:`Require Lib.Foo.File`, :n:`From Lib Require Foo.File`,
@@ -559,18 +558,18 @@ file is a particular case of a module called a *library file*.
    package or subpackage.  Use of `-Q` is better for avoiding ambiguous
    path names.
 
-   When looking for a file :n:`@dirpath.{* @ident__implicit. }@qualid` or
-   :n:`{* @ident__implicit. }@qualid`,
-   exact matches are preferred (that is, matches where the implicit part
-   is empty). If the name exactly matches in
-   multiple `-R` or `-Q` options, the file corresponding to the most
-   recent `-R` or `-Q` is used. If there is no exact match, the
+   Exact matches are preferred when looking for a file with the logical name
+   :n:`@dirpath.{* @ident__implicit. }@qualid` or
+   :n:`{* @ident__implicit. }@qualid`
+   (that is, matches where the implicit part is empty). If the name exactly
+   matches in multiple `-R` or `-Q` options, the file corresponding to the most
+   recent `-R` or `-Q` is used.  If there is no exact match, the
    matches from the most recent `-R` or `-Q` are selected. If this
    results in a unique match, the corresponding file is selected. If
    this results in several matches, it is an error. The difference
    between the `-R` and the `-Q` option is that non-exact matches are
    allowed for `-Q` only if `From` is present, that is if a prefix is
-   given.  Matching is done when only the script is compiled
+   given.  Matching is done when the script is compiled
    or processed rather than when its .vo file is loaded.  .vo files use
    fully-qualified names.