From 2f0e71c7e25eb193f252b6848dadff771dbc270d Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 2 Aug 2017 09:42:37 +0200
Subject: Typo in the documentation of cumulativity

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

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 667fd66984..cd36d1d320 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -173,17 +173,17 @@ convertible if and only if \texttt{i $=$ j}.
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the \texttt{Cumulative} or
-\texttt{NonCumulative} prefix in a monomorphic contexts.
+\texttt{NonCumulative} prefix in a monomorphic context.
 Notice that this is not the case for the option \texttt{Set Polymorphic Inductive Cumulativity}.
-That is, this optiotion, when set, makes all subsequent \emph{polymorphic}
-inductive declarations cumulative (unless, of course if the \texttt{NonCumulative} prefix is used)
+That is, this option, when set, makes all subsequent \emph{polymorphic}
+inductive declarations cumulative (unless, of course the \texttt{NonCumulative} prefix is used)
 but has no effect on \emph{monomorphic} inductive declarations.
 Consider the following examples.
 \begin{coq_example}
-Fail Monomorphic Cumulative Inductive Unit := unit.
+Monomorphic Cumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example}
-Fail Monomorphic NonCumulative Inductive Unit := unit.
+Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example*}
 Set Polymorphic Inductive Cumulativity.
-- 
cgit v1.2.3