diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-05 14:48:03 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-05 16:48:29 +0100 |
| commit | 0e35acf14e0289b5a531d385eaf0506db4430da4 (patch) | |
| tree | 1572f00cfa9f7516e397cc5311d6ccd77ea436c8 /doc | |
| parent | 2c0f1eb6f9a6e16b2b4d3a99542df7f49c81f6ea (diff) | |
Fix some documentation typos.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index ce230a0f7..40e0ecc11 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -308,9 +308,9 @@ statement's conclusion has the form {\tt ({\term} t1 .. tn)}. This command is useful to remind the user of the name of library lemmas. -\begin{coq_example*} +\begin{coq_eval} Reset Initial. -\end{coq_example*} +\end{coq_eval} \begin{coq_example} SearchHead le. diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 11954ed0e..24417bd03 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -120,7 +120,7 @@ is on Figure~\ref{init-notations}. \subsection{Complex notations} -Notations can be made from arbitraly complex symbols. One can for +Notations can be made from arbitrarily complex symbols. One can for instance define prefix notations. \begin{coq_example*} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 48e2df19d..76e4efd60 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -68,7 +68,7 @@ but also at the command {\tt Declare ML Module}. Dependencies of \ocaml\ modules are computed by looking at \verb!open! commands and the dot notation {\em module.value}. However, -this is done approximatively and you are advised to use {\tt ocamldep} +this is done approximately and you are advised to use {\tt ocamldep} instead for the \ocaml\ modules dependencies. See the man page of {\tt coqdep} for more details and options. @@ -103,7 +103,7 @@ invocation While customizing a project file, mind the following requirements: \begin{itemize} \item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in - \texttt{.ml4} if they require camlp preproccessing (and in + \texttt{.ml4} if they require camlp preprocessing (and in \texttt{.ml} otherwise), {\ocaml} module signatures, library description and packing files respectively in \texttt{.mli}, \texttt{.mllib} and \texttt{.mlpack}. |