From 7104904f9f6e1a5e1b1590bd898ae20cb7178daf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:29:39 +0100
Subject: Fix failing coqtops universe-polymorphism.rst

---
 doc/sphinx/addendum/universe-polymorphism.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 04aedd0cf6..6b10b7c0b3 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -223,7 +223,7 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
-Cumulative inductive types, coninductive types, variants and records
+Cumulative inductive types, coinductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the :g:`Cumulative` or
 :g:`NonCumulative` prefix in a monomorphic context.
@@ -236,11 +236,11 @@ Consider the following examples.
 
 .. coqtop:: all reset
 
-   Monomorphic Cumulative Inductive Unit := unit.
+   Fail Monomorphic Cumulative Inductive Unit := unit.
 
 .. coqtop:: all reset
 
-   Monomorphic NonCumulative Inductive Unit := unit.
+   Fail Monomorphic NonCumulative Inductive Unit := unit.
 
 .. coqtop:: all reset
 
-- 
cgit v1.2.3