diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 24 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 42 |
3 files changed, 36 insertions, 36 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 49bcdb1db..e4c6be715 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}]]\ 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}]\ diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 85f191104..cc5239a77 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1059,7 +1059,7 @@ names to {\Coq} names is needed. In this translation, names in the file system are called {\em physical} paths while {\Coq} names are contrastingly called {\em logical} names. -A logical prefix {\tt Lib} can associated to a physical path +A logical prefix {\tt Lib} can be associated to a physical path \textrm{\textsl{path}} using the command line option {\tt -Q} \textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are recursively associated to the logical path {\tt Lib} extended with the @@ -1102,8 +1102,8 @@ root to the required file (see~\ref{Require}). 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}. +\texttt{-I path} (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. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 85deb3175..4952ed778 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -4,7 +4,7 @@ \section{Displaying} \subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}} -This command displays on the screen informations about the declared or +This command displays on the screen information about the declared or defined object referred by {\qualid}. \begin{ErrMsgs} @@ -20,7 +20,7 @@ global constant. \item {\tt About {\qualid}.} \label{About} \comindex{About}\\ -This displays various informations about the object denoted by {\qualid}: +This displays various information about the object denoted by {\qualid}: its kind (module, constant, assumption, inductive, constructor, abbreviation, \ldots), long name, type, implicit arguments and argument scopes. It does not print the body of @@ -34,7 +34,7 @@ definitions or proofs. \end{Variants} \subsection[\tt Print All.]{\tt Print All.\comindex{Print All}} -This command displays informations about the current state of the +This command displays information about the current state of the environment, including sections and modules. \begin{Variants} @@ -183,7 +183,7 @@ displayed as in \Coq\ terms. \begin{Variants} \item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\ Recursively extracts all the material needed for the extraction of - globals {\qualid$_1$}, \ldots, {\qualid$_n$}. + global {\qualid$_1$}, \ldots, {\qualid$_n$}. \end{Variants} \SeeAlso Chapter~\ref{Extraction}. @@ -294,7 +294,7 @@ Search "+"%Z "*"%Z "distr" -positive -Prop. Search (?x * _ + ?x * _)%Z outside OmegaLemmas. \end{coq_example} -\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search} +\Warning \comindex{SearchAbout} Up to {\Coq} version 8.4, {\tt Search} had the behavior of current {\tt SearchHead} and the behavior of current {\tt Search} was obtained with command {\tt SearchAbout}. For compatibility, the deprecated name {\tt SearchAbout} can still be used @@ -343,7 +343,7 @@ No module \module{} has been required (see Section~\ref{Require}). \end{Variants} -\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}. +\Warning Up to {\Coq} version 8.4, {\tt SearchHead} was named {\tt Search}. \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}} @@ -458,8 +458,8 @@ The default blacklisted substrings are {\tt \label{Locate}} This command displays the full name of objects whose name is a prefix of the qualified identifier {\qualid}, and consequently the \Coq\ module in which they -are defined. It searches for objects from the different qualified namespaces of -Coq: terms, modules, Ltac, etc. +are defined. It searches for objects from the different qualified name spaces of +{\Coq}: terms, modules, Ltac, etc. \begin{coq_eval} (*************** The last line should produce **************************) @@ -593,7 +593,7 @@ is picked in an unspecified fashion. 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. + package by making explicit its absolute root. \end{Variants} @@ -620,7 +620,7 @@ is picked in an unspecified fashion. \index{Bad-magic-number@{\tt Bad Magic Number}} The file {\tt{\ident}.vo} was found but either it is not a \Coq\ compiled module, or it was compiled with an older and incompatible - version of \Coq. + version of {\Coq}. \item \errindex{The file {\ident}.vo contains library {\dirpath} and not library {\dirpath'}} @@ -657,7 +657,7 @@ searched into the current {\ocaml} loadpath (see the command {\tt Add ML Path} in the Section~\ref{loadpath}). Loading of {\ocaml} files is only possible under the bytecode version of {\tt coqtop} (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter -\ref{Addoc-coqc}), or when Coq has been compiled with a version of +\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11). \begin{Variants} @@ -668,7 +668,7 @@ files is only possible under the bytecode version of {\tt coqtop} \begin{ErrMsgs} \item \errindex{File not found on loadpath : \str} -\item \errindex{Loading of ML object file forbidden in a native Coq} +\item \errindex{Loading of ML object file forbidden in a native {\Coq}} \end{ErrMsgs} \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}} @@ -679,7 +679,7 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File}) \section[Loadpath]{Loadpath} Loadpaths are preferably managed using {\Coq} command line options -(see Section~\ref{loadpath}) but there remains vernacular commands to +(see Section~\ref{loadpath}) but there remain vernacular commands to manage them. \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}} @@ -696,7 +696,7 @@ which can be any valid path. \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}} -This command is equivament to the command line option {\tt -Q {\dirpath} +This command is equivalent to the command line option {\tt -Q {\dirpath} {\str}}. It adds the physical directory {\str} to the current {\Coq} loadpath and maps it to the logical directory {\dirpath}. @@ -778,11 +778,11 @@ over the name of a module or of an object inside a module. This commands undoes all the effects of the last vernacular command. Commands read from a vernacular file via a {\tt Load} are -considered as a single command. Proof managment commands +considered as a single command. Proof management commands are also handled by this command (see Chapter~\ref{Proof-handling}). For that, {\tt Back} may have to undo more than one command in order -to reach a state where the proof managment information is available. -For instance, when the last command is a {\tt Qed}, the managment +to reach a state where the proof management information is available. +For instance, when the last command is a {\tt Qed}, the management information about the closed proof has been discarded. In this case, {\tt Back} will then undo all the proof steps up to the statement of this proof. @@ -803,7 +803,7 @@ this proof. \subsection[\tt BackTo $\num$.]{\tt BackTo $\num$.\comindex{BackTo}} \label{sec:statenums} -This command brings back the system to the state labelled $\num$, +This command brings back the system to the state labeled $\num$, forgetting the effect of all commands executed after this state. The state label is an integer which grows after each successful command. It is displayed in the prompt when in \texttt{-emacs} mode. @@ -814,14 +814,14 @@ extra commands and end on a state $\num' \leq \num$ if necessary. \begin{Variants} \item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\ {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which - allows explicitely manipulating the proof environment. The three + allows explicitly manipulating the proof environment. The three numbers $\num_1$, $\num_2$ and $\num_3$ represent the following: \begin{itemize} \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number of currently opened nested proofs that must be canceled (see Chapter~\ref{Proof-handling}). \item $\num_2$: \emph{Proof state number} to unbury once aborts have - been done. Coq will compute the number of \texttt{Undo} to perform + been done. {\Coq} will compute the number of \texttt{Undo} to perform (see Chapter~\ref{Proof-handling}). \item $\num_1$: State label to reach, as for {\tt BackTo}. \end{itemize} @@ -949,7 +949,7 @@ algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode representation used in the ZINC virtual machine~\cite{Leroy90}. It is especially useful for intensive -computation of algebraic values, such as numbers, and for reflexion-based +computation of algebraic values, such as numbers, and for reflection-based tactics. The commands to fine-tune the reduction strategies and the lazy conversion algorithm are described first. |