Documenting "From * Require *" and clearing a bit the loadpath chapter.

2 files changed, 45 insertions, 28 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d1ce3bf41..ca240ff04 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1061,42 +1061,49 @@ contrastingly called {\em logical} names.
 
 A logical name {\tt Lib} can associated to a physical path
 \textrm{\textsl{path}} using the command line option {\tt -Q}
-\textrm{\textsl{path}} {\tt Lib}. This associates a logical name to
-all the compiled files in the directory tree rooted at
-\textrm{\textsl{path}}. The name associated to the file {\tt
-  path/fOO/Bar/File.vo} is {\tt Lib.fOO.Bar.File}. Subdirectories
+\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
+recursively associated to the logical path {\tt Lib} extended with the
+corresponding suffix coming from the physical path. For instance, the
+folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories
 corresponding to invalid {\Coq} identifiers are skipped, and, by
 convention, subdirectories named {\tt CVS} or {\tt \_darcs} are
 skipped too.
 
-{\Coq} commands also associate automatically a logical path to files
+Thanks to this mechanism, {\texttt{.vo}} files are made available through the
+logical name of the folder they are in, extended with their own basename. For
+example, the name associated to the file {\tt path/fOO/Bar/File.vo} is
+{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers.
+
+Some folders have a special status and are automatically put in the path.
+{\Coq} commands associate automatically a logical path to files
 in the repository trees rooted at the directory from where the command
 is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories
 listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and
 \verb:${XDG_DATA_DIRS}/coq/: environment variables (see
 \url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html})
-with the same $/ \to .$ convention but no prefix.
-
-The command line option \texttt{-R} is a variant of \texttt{-Q} that
-associates to a physical path the same logical path as \texttt{-Q}, as
-well as all suffixes of that logical path. The option \texttt{-R}
-\textrm{\textsl{path}} \texttt{Lib} associates to
-\texttt{path/fOO/Bar/File.vo} the logical names
-\texttt{Lib.fOO.Bar.File}, \texttt{fOO.Bar.File}, \texttt{Bar.File}
-and \texttt{File}. If several files with identical base name are
-present in different subdirectories of a recursive loadpath, which of
+with the same physical-to-logical translation and with an empty logical prefix.
+
+The command line option \texttt{-R} is a variant of \texttt{-Q} which has the
+strictly same behavior regarding loadpaths, but which also makes the
+corresponding \texttt{.vo} files available through their short names in a
+way not unlike the {\tt Import} command~(see {\ref{Import}}). For instance,
+\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file
+\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but
+allows this file to be accessed through the short names \texttt{fOO.Bar.File},
+\texttt{Bar.File} and \texttt{File}. If several files with identical base name
+are present in different subdirectories of a recursive loadpath, which of
 these files is found first may be system-dependent and explicit
-qualification is recommended.
-
-There are currently two loadpaths in {\Coq}. There is one loadpath
-where seeking {\Coq} files (extensions \texttt{.v} or \texttt{.vo} or
-\texttt{.vi}) whose management has been explained just above, and one
-where seeking {\ocaml} files. The {\ocaml} loadpath is
-managed using the option \texttt{-I path}. As in {\ocaml} world, there
-is nether a notion of logical name prefix nor a way to access files in
-subdirectories of \texttt{path}. See the command \texttt{Declare ML
-  Module} in Section~\ref{compiled} to understand the need of the
-{\ocaml} loadpath.
+qualification is recommended. The {\tt From} argument of the {\tt Require}
+command can be used to bypass the implicit shortening by providing an absolute
+root to the required file.
+
+There also exists another independent loadpath mechanism attached to {\ocaml}
+object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
+as described above. The {\ocaml} loadpath is managed using the option
+\texttt{-I path}. As in the {\ocaml} world, there is neither a notion of logical
+name prefix nor a way to access files in subdirectories of \texttt{path}.
+See the command \texttt{Declare ML Module} in Section~\ref{compiled} to
+understand the need of the {\ocaml} loadpath.
 
 See Section~\ref{coqoptions} for a more general view over the {\Coq}
 command line options.
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 556a2dab5..85deb3175 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -553,10 +553,11 @@ the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
 mapped in {\Coq} loadpath to the logical path {\dirpath} (see
 Section~\ref{loadpath}). The mapping between physical directories and
 logical names at the time of requiring the file must be consistent
-with the mapping used to compile the file.
+with the mapping used to compile the file. If several files match, one of them
+is picked in an unspecified fashion.
 
 \begin{Variants}
-\item {\tt Require Import {\qualid}.} \comindex{Require} 
+\item {\tt Require Import {\qualid}.} \comindex{Require Import}
 
   This loads and declares the module {\qualid} and its dependencies
   then imports the contents of {\qualid} as described in
@@ -585,6 +586,15 @@ with the mapping used to compile the file.
   given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all
   the recursive dependencies that were marked or transitively marked
   as {\tt Export}.
+
+\item {\tt From {\dirpath} Require {\qualid}.}
+  \comindex{From Require}
+
+  This command acts as {\tt Require}, but picks any library whose absolute name
+  is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}.
+  This is useful to ensure that the {\qualid} library comes from a given
+  package by expliciting its absolute root.
+
 \end{Variants}
 
 \begin{ErrMsgs}