From 81b43a0c8137dc890fe1eb462cf278c39cac3a5f Mon Sep 17 00:00:00 2001
From: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
Date: Fri, 29 Aug 2014 18:17:54 +0200
Subject: Update RefMan with respect to new loadpath management

---
 doc/refman/RefMan-com.tex | 44 +++++++++++++++++++++++++-------------------
 1 file changed, 25 insertions(+), 19 deletions(-)

(limited to 'doc/refman/RefMan-com.tex')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 3feabb228..96b93a8c0 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -67,13 +67,15 @@ option \verb:-q:.
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
-\verb:$COQPATH: environment variable. It is a list of directories separated by \verb|:|
-(\verb|;| on windows).
+\verb:$COQPATH: environment variable. It is a list of directories
+separated by \verb|:| (\verb|;| on windows). {\Coq} will also honour
+\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see section
+\ref{loadpath}).
 
-\Coq will also honour \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see
-\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}).
-\Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its
-search path.
+Some {\Coq} commands call other {\Coq} commands. In this case, they
+look for the commands in directory specified by \verb:$COQBIN:. If
+this variable is not set, they look for the command in the executable
+path.
 
 \subsection{By command line options\index{Options of the command line}
 \label{vmoption}
@@ -83,26 +85,30 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}[ {\tt -as} {\em dirpath}]]\ 
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
 
-Add physical path {\em directory} to the list of directories where to look for a
-file and bind it to the empty logical directory/the logical directory {\em
-  dirpath}. The sub-directory structure of {\em directory} is recursively available
-from {\Coq} using absolute names (extending the {\dirpath} prefix) (see
-Section~\ref{LongNames}).
+Add physical path {\em directory} to the Objective Caml loadpath.
 
-  \SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical
-  paths in Section~\ref{Libraries}.
+  \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
+
+\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+
+  Add physical path \emph{directory} to the list of directories where
+  {\Coq} looks for a file and bind it to the the logical directory
+  \emph{dirpath}. The sub-directory structure of \emph{directory} is
+  recursively available from {\Coq} using absolute names (extending
+  the {\dirpath} prefix) (see Section~\ref{LongNames}).
+  
+  \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\
 
-  Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the
-  sub-directory structure of {\em directory} recursively visible so
-  that the recursive contents of physical {\em directory} is available
+  Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
+  sub-directory structure of \emph{directory} recursively visible so
+  that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
   
-  \SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical
-  paths in Section~\ref{Libraries}.
+  \SeeAlso Section~\ref{Libraries}.
 
 \item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
 
-- 
cgit v1.2.3