diff options
Diffstat (limited to 'doc/refman/Universes.tex')
| -rw-r--r-- | doc/refman/Universes.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 7de74ef95..ccd180db6 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -7,7 +7,7 @@ \asection{General Presentation} This section describes the universe polymorphic extension of Coq. -Universe polymorphism allows to write generic definitions making use of +Universe polymorphism allows writing generic definitions making use of universes and reuse them at different and sometimes incompatible levels. A standard example of the difference between universe \emph{polymorphic} and |