aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-com.tex
diff options
context:
space:
mode:
authorPierre Letouzey2015-04-09 14:46:37 +0200
committerPierre Letouzey2015-04-09 14:46:37 +0200
commit429f493997e34bfaac930c68bf6b267a5b9640ee (patch)
tree28f15d0aeff2ce899a312f31e10fe2030b2dd813 /doc/refman/RefMan-com.tex
parentaeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff)
parenteaa3f9719d6190ba92ce55816f11c70b30434309 (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'doc/refman/RefMan-com.tex')
-rw-r--r--doc/refman/RefMan-com.tex26
1 files changed, 13 insertions, 13 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 49bcdb1db7..6335dfd324 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -29,9 +29,9 @@ for your platform, which is supposed in the following). By default,
\verb!coqc! executes the native-code version; this can be overridden
using the \verb!-byte! option.
-The byte-code toplevel is based on a Caml
+The byte-code toplevel is based on an {\ocaml}
toplevel (to allow the dynamic link of tactics). You can switch to
-the Caml toplevel with the command \verb!Drop.!, and come back to the
+the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the
\Coq~toplevel with the command \verb!Toplevel.loop();;!.
\section{Batch compilation ({\tt coqc})}
@@ -69,13 +69,13 @@ option \verb:-q:.
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). {\Coq} will also honour
-\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see section
+separated by \verb|:| (\verb|;| on windows). {\Coq} will also honor
+\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see Section
\ref{loadpath}).
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
+this variable is not set, they look for the commands in the executable
path.
The \verb:$COQ_COLORS: environment variable can be used to specify the set of
@@ -104,16 +104,16 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
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
+ \emph{dirpath}. The subdirectory 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}]]\
+\item[{\tt -R} {\em directory} {\dirpath}]\
Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
- sub-directory structure of \emph{directory} recursively visible so
+ subdirectory 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.
@@ -126,9 +126,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
\item[{\tt -exclude-dir} {\em subdirectory}]\
- This tells to exclude any sub-directory named {\em subdirectory}
+ This tells to exclude any subdirectory named {\em subdirectory}
while processing option {\tt -R}. Without this option only the
- conventional version control management sub-directories named {\tt
+ conventional version control management subdirectories named {\tt
CVS} and {\tt \_darcs} are excluded.
\item[{\tt -nois}]\
@@ -142,11 +142,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
\item[{\tt -load-ml-source} {\em file}]\
- Load the Caml source file {\em file}.
+ Load the {\ocaml} source file {\em file}.
\item[{\tt -load-ml-object} {\em file}]\
- Load the Caml object file {\em file}.
+ Load the {\ocaml} object file {\em file}.
\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\