From 0e35acf14e0289b5a531d385eaf0506db4430da4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 5 Feb 2015 14:48:03 +0100
Subject: Fix some documentation typos.

---
 doc/refman/RefMan-oth.tex | 4 ++--
 doc/refman/RefMan-syn.tex | 2 +-
 doc/refman/RefMan-uti.tex | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc')

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}.
-- 
cgit v1.2.3