Fix some typos.

1 files changed, 8 insertions, 8 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fbb866e875..2eebac39ac 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.