Fix some typos.

2 files changed, 5 insertions, 5 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 2eebac39ac..48b61827d1 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -710,7 +710,7 @@ There are also ``simple enough'' propositions for which you can prove
 the equality without requiring any extra axioms.  This is typically
 the case for propositions defined deterministically as a first-order
 inductive predicate on decidable sets. See for instance in question
-\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of
+\ref{le-uniqueness} an axiom-free proof of the uniqueness of the proofs of
 the proposition {\tt le m n} (less or equal on {\tt nat}).
 
 %  It is an ongoing work of research to natively include proof
@@ -1625,7 +1625,7 @@ Fail Definition max (n p : nat) := if n <= p then p else n.
 As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
 statement that belongs to the mathematical world. There are many ways to
 prove such a proposition, either by some computation, or using some already
-proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
+proven theorems. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
 using some theorems on arithmetical operations. If you compute both numbers
 before comparing them, you risk to use a lot of time and space.
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a03d5c7b20..cd8222269d 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -183,7 +183,7 @@ bound if it is an atomic universe (i.e. not an algebraic max()).
 \end{flushleft}
 
 The syntax has been extended to allow users to explicitly bind names to
-universes and explicitly instantantiate polymorphic
+universes and explicitly instantiate 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. 
@@ -200,7 +200,7 @@ we are using $A : Type@{i} <= Type@{j}$, hence the generated
 constraint. Note that the names here are not bound in the final
 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.
+introduced in the types can be referred to in terms.
 
 Definitions can also be instantiated explicitly, giving their full instance:
 \begin{coq_example}
@@ -209,7 +209,7 @@ Check (le@{i j}).
 \end{coq_example}
 
 User-named universes are considered rigid for unification and are never
-miminimized.
+minimized.
 
 Finally, two commands allow to name \emph{global} universes and constraints.