diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-14 10:39:55 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-14 10:39:55 +0200 |
| commit | f617aeef08441e83b13f839ce767b840fddbcf7d (patch) | |
| tree | 9a0c914031262f5491745d9773d7c2a0e5bdaa41 /doc/refman | |
| parent | ed95f122f3c68becc09c653471dc2982b346d343 (diff) | |
Fix some typos.
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Universes.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index a03d5c7b2..cd8222269 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. |