From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 doc/refman/Universes.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 018d73908b..a03d5c7b20 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}).
-- 
cgit v1.2.3


From f617aeef08441e83b13f839ce767b840fddbcf7d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 14 Oct 2015 10:39:55 +0200
Subject: Fix some typos.

---
 doc/refman/Universes.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman')

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