Fix some typos.

3 files changed, 12 insertions, 12 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fbb866e87..2eebac39a 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -228,7 +228,7 @@ kernel is intentionally small to limit the risk of conceptual or
 accidental implementation bugs.
 \item[The Objective Caml compiler] The {\Coq} kernel is written using the
 Objective Caml language but it uses only the most standard features
-(no object, no label ...), so that it is highly unprobable that an
+(no object, no label ...), so that it is highly improbable that an
 Objective Caml bug breaks the consistency of {\Coq} without breaking all
 other kinds of features of {\Coq} or of other software compiled with
 Objective Caml.
@@ -1497,7 +1497,7 @@ while {\assert} is.
 
 \Question{What can I do if \Coq can not infer some implicit argument ?}
 
-You can state explicitely what this implicit argument is. See \ref{implicit}.
+You can state explicitly what this implicit argument is. See \ref{implicit}.
 
 \Question{How can I explicit some implicit argument ?}\label{implicit}
 
@@ -1632,7 +1632,7 @@ before comparing them, you risk to use a lot of time and space.
 
 On the contrary, a function for computing the greatest of two natural numbers
 is an algorithm  which, called on two natural numbers
-$n$ and $p$, determines wether $n\leq p$ or $p < n$.
+$n$ and $p$, determines whether $n\leq p$ or $p < n$.
 Such a function is a \emph{decision  procedure} for the inequality of
  \texttt{nat}.  The possibility of writing such a procedure comes 
 directly from de decidability of the order $\leq$ on natural numbers.
@@ -1706,7 +1706,7 @@ immediate, whereas one can't wait for  the result of
 
 This is normal. Your definition is a simple recursive function which
 returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
-function}, i.e. a complex object, able not only to tell wether $n\leq p$
+function}, i.e. a complex object, able not only to tell whether $n\leq p$
 or $p<n$, but also of building a complete proof of the correct inequality.
 What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
 and \texttt{max} is the building of a huge proof term.
@@ -2404,8 +2404,8 @@ You can use {\tt coqdoc}.
 
 \Question{How can I generate some dependency graph from my development?}
 
-You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
-This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
+You can use the tool \verb|coqgraph| developed by Philippe Audebaud in 2002.
+This tool transforms dependencies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
 
 \Question{How can I cite some {\Coq} in my latex document?}
 
@@ -2539,7 +2539,7 @@ modifiers keys available through GTK. The straightest way to get
 rid of the problem is to edit by hand your coqiderc (either
 \verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
 \verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) 
-    and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.
+and replace any occurrence of \texttt{MOD4} by \texttt{MOD1}.
 
 
 
@@ -2638,7 +2638,7 @@ existential variable which eventually got erased by some computation.
 You may backtrack to the faulty occurrence of {\eauto} or {\eapply}
 and give the missing argument an explicit value. Alternatively, you
 can use the commands \texttt{Show Existentials.} and
-\texttt{Existential.} to display and instantiate the remainig
+\texttt{Existential.} to display and instantiate the remaining
 existential variables.
 
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 018d73908..a03d5c7b2 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -182,8 +182,8 @@ bound if it is an atomic universe (i.e. not an algebraic max()).
   experimental and is likely to change in future versions.
 \end{flushleft}
 
-The syntax has been extended to allow users to explicitely bind names to
-universes and explicitely instantantiate polymorphic
+The syntax has been extended to allow users to explicitly bind names to
+universes and explicitly instantantiate polymorphic
 definitions. Currently, binding is implicit at the first occurrence of a 
 universe name. For example, i and j below are introduced by the
 annotations attached to Types. 
@@ -202,7 +202,7 @@ definition, they just allow to specify locally what relations should
 hold. In the term and in general in proof mode, universe names
 introduced in the types can be refered to in terms.
 
-Definitions can also be instantiated explicitely, giving their full instance:
+Definitions can also be instantiated explicitly, giving their full instance:
 \begin{coq_example}
 Check (pidentity@{Set}).
 Check (le@{i j}).
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 5f7b6dc95..ed1d336d9 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -419,7 +419,7 @@ the hypotheses), or a comma-separated list of either hypothesis name,
 or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences
 can be specified after every hypothesis after the {\TERM{at}}
 keyword. {\em concl} is either empty or \TERM{*}, and can be followed
-by occurences.
+by occurrences.
 
 \begin{transbox}
 \TRANS{in Goal}{in |- *}