From fbe0b2645eab84012aec50e76d94e15a3fefe664 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:09:31 +0200
Subject: Issue error on monomorphic cumulative inductives

---
 test-suite/success/cumulativity.v | 6 ++++++
 vernac/vernacentries.ml           | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index ebf817cfc5..604da2108e 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -1,3 +1,9 @@
+Polymorphic Cumulative Inductive T1 := t1 : T1.
+Fail Monomorphic Cumulative Inductive T2 := t2 : T2.
+
+Polymorphic Cumulative Record R1 := { r1 : T1 }.
+Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
+
 Set Universe Polymorphism.
 Set Inductive Cumulativity.
 Set Printing Universes.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6b04ff00a0..3542c4081e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,7 +522,12 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
+let check_cumulativity_polymorphism_flag cum poly =
+  if cum && not poly then 
+    user_err Pp.(str "Monomorphic cumulative inductive types/records are not supported. ")
+
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
+  check_cumulativity_polymorphism_flag cum poly;
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -540,6 +545,7 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive cum poly lo finite indl =
+  check_cumulativity_polymorphism_flag cum poly;
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
-- 
cgit v1.2.3


From 7f78827b3f8583a7c0e79a78266bc01a411ed818 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 14:26:05 +0200
Subject: Add test for NonCumulative inductives

---
 test-suite/success/cumulativity.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 604da2108e..351d472a11 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -68,4 +68,16 @@ End subtyping_test.
 
 Record A : Type := { a :> Type; }.
 
-Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
+Record B (X : A) : Type := { b : X; }.
+
+NonCumulative Inductive NCList (A: Type)
+  := ncnil | nccons : A -> NCList A -> NCList A.
+
+Section NCListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
+
+End NCListLift.
-- 
cgit v1.2.3


From 9f0abdf5d9f3dde45758c8b9fe0fbe86eef01ee2 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 15:41:41 +0200
Subject: Add Jason's example of fun-ext with cumulativity

---
 test-suite/success/cumulativity.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 351d472a11..8854435cf3 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -81,3 +81,20 @@ Section NCListLift.
   Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
 
 End NCListLift.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    : @funext_type@{a b e} A B -> @funext_type@{a b e'} A B.
+  Proof.
+    intros H f g Hfg. exact (H f g Hfg).
+  Defined.
+End down.
-- 
cgit v1.2.3


From 77d4c058261e6e843a4a80f7f0290c4798d0f5ec Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 16:31:04 +0200
Subject: Improve documentation of cumulativity

---
 doc/refman/Universes.tex | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 2bb1301c79..79b9e4df52 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -139,7 +139,9 @@ producing global universe constraints, one can use the
 Inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
 there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative. Consider the examples below.
+makes all subsequent inductive definitions cumulative.  When set
+inductive types and the like can be enforced to be
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
 Polymorphic Cumulative Inductive list {A : Type} :=
 | nil : list
@@ -176,6 +178,25 @@ Print packType.
 \end{coq_example}
 Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are 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 inputs such monomorphic and
+cumulative type. Notice that this also implies that when the option
+\texttt{Set Inductive Cumulativity} is set any subsequent inductive
+declaration should be polymorphic, e.g., by setting \texttt{Set
+  Universe Polymorphism}, unless it is specifically made
+\emph{non-cumulative} using the \texttt{NonCumulative} prefix.
+
+\begin{coq_example}
+Fail Monomorphic Cumulative Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+Set Inductive Cumulativity.
+Fail Inductive Unit := unit.
+\end{coq_example}
+\begin{coq_example}
+NonCumulative Inductive Unit := unit.
+\end{coq_example}
 
 \asection{Global and local universes}
 
-- 
cgit v1.2.3


From 28998d55aaaf0ad0e78477db5601a5bc9a6657b1 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Jul 2017 17:57:01 +0200
Subject: Fix typo and Add Jason's example to the doc

---
 doc/refman/Universes.tex | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 79b9e4df52..e097de59b3 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -139,7 +139,7 @@ producing global universe constraints, one can use the
 Inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
 there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative.  When set
+makes all subsequent inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
 \emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
@@ -180,7 +180,7 @@ Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
 
 Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
-error is issued whenever the user inputs such monomorphic and
+error is issued whenever the user inputs such a monomorphic and
 cumulative type. Notice that this also implies that when the option
 \texttt{Set Inductive Cumulativity} is set any subsequent inductive
 declaration should be polymorphic, e.g., by setting \texttt{Set
@@ -198,6 +198,29 @@ Fail Inductive Unit := unit.
 NonCumulative Inductive Unit := unit.
 \end{coq_example}
 
+\subsection*{An example of a proof using cumulativity}
+
+\begin{coq_example}
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+
+Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
+
+Definition funext_type@{a b e} (A : Type@{a}) (B : A -> Type@{b})
+  := forall f g : (forall a, B a),
+    (forall x, eq@{e} (f x) (g x))
+    -> eq@{e} f g.
+
+Section down.
+  Universes a b e e'.
+  Constraint e' < e.
+  Lemma funext_down {A B}
+    (H : @funext_type@{a b e} A B) : @funext_type@{a b e'} A B.
+  Proof.
+    exact H.
+  Defined.
+\end{coq_example}
+
 \asection{Global and local universes}
 
 Each universe is declared in a global or local environment before it can
-- 
cgit v1.2.3


From 3b7e7f7738737475cb0f09130b0487c85906dd2b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 13:29:36 +0200
Subject: Change the option for cumulativity

---
 lib/flags.ml                      | 6 +++---
 lib/flags.mli                     | 6 +++---
 parsing/g_vernac.ml4              | 2 +-
 test-suite/coqchk/cumulativity.v  | 2 +-
 test-suite/success/cumulativity.v | 2 +-
 vernac/vernacentries.ml           | 8 ++++----
 6 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/lib/flags.ml b/lib/flags.ml
index 0bce22f584..027ba16f0e 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -167,9 +167,9 @@ let use_polymorphic_flag () =
 let make_polymorphic_flag b =
   local_polymorphic_flag := Some b
 
-let inductive_cumulativity = ref false
-let make_inductive_cumulativity b = inductive_cumulativity := b
-let is_inductive_cumulativity () = !inductive_cumulativity
+let polymorphic_inductive_cumulativity = ref false
+let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
+let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
 
 (** [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
diff --git a/lib/flags.mli b/lib/flags.mli
index eb4c37a548..5af563b46e 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,9 +119,9 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
-(** Global inductive cumulativity flag. *)
-val make_inductive_cumulativity : bool -> unit
-val is_inductive_cumulativity : unit -> bool
+(** Global polymorphic inductive cumulativity flag. *)
+val make_polymorphic_inductive_cumulativity : bool -> unit
+val is_polymorphic_inductive_cumulativity : unit -> bool
 
 val warn : bool ref
 val make_warn : bool -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d29fca779..568818c270 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -169,7 +169,7 @@ GEXTEND Gram
 	  let cum =
 	    match cum with
 	      Some b -> b
-	    | None -> Flags.is_inductive_cumulativity ()
+	    | None -> Flags.is_polymorphic_inductive_cumulativity ()
 	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index a978f6b901..7906a5b15e 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 8854435cf3..0ee85712e2 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -5,7 +5,7 @@ Polymorphic Cumulative Record R1 := { r1 : T1 }.
 Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}.
 
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3542c4081e..12a31953c5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1369,10 +1369,10 @@ let _ =
 let _ =
   declare_bool_option
     { optdepr  = false;
-      optname  = "inductive cumulativity";
-      optkey   = ["Inductive"; "Cumulativity"];
-      optread  = Flags.is_inductive_cumulativity;
-      optwrite = Flags.make_inductive_cumulativity }
+      optname  = "Polymorphic inductive cumulativity";
+      optkey   = ["Polymorphic"; "Inductive"; "Cumulativity"];
+      optread  = Flags.is_polymorphic_inductive_cumulativity;
+      optwrite = Flags.make_polymorphic_inductive_cumulativity }
 
 let _ =
   declare_int_option
-- 
cgit v1.2.3


From e333c2fa6d97e79b389992412846adc71eb7abda Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 17:41:38 +0200
Subject: Improve errors for cumulativity when monomorphic

We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
---
 API/API.mli                             |  8 +++++++-
 intf/vernacexpr.ml                      | 10 +++++++++-
 parsing/g_vernac.ml4                    |  9 +++++++--
 plugins/funind/glob_term_to_relation.ml |  4 ++--
 printing/ppvernac.ml                    |  6 +++++-
 vernac/vernacentries.ml                 | 23 ++++++++++++++++-------
 6 files changed, 46 insertions(+), 14 deletions(-)

diff --git a/API/API.mli b/API/API.mli
index 19726b52f2..d39d3cb25c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3780,6 +3780,12 @@ sig
     | DefaultInline
     | InlineAt of int
 
+  type cumulative_inductive_parsing_flag =
+    | GlobalCumulativity
+    | GlobalNonCumulativity
+    | LocalCumulativity
+    | LocalNonCumulativity
+
   type vernac_expr =
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_expr Loc.located
@@ -3804,7 +3810,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 6ef9532ad7..2adf522b74 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -305,6 +305,14 @@ type inline =
 type module_ast_inl = module_ast * inline
 type module_binder = bool option * lident list * module_ast_inl
 
+(** Cumulativity can be set globally, locally or unset locally and it
+   can not enabled at all. *)
+type cumulative_inductive_parsing_flag =
+  | GlobalCumulativity
+  | GlobalNonCumulativity
+  | LocalCumulativity
+  | LocalNonCumulativity
+
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
@@ -336,7 +344,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 568818c270..93a778274d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -168,8 +168,13 @@ GEXTEND Gram
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
 	  let cum =
 	    match cum with
-	      Some b -> b
-	    | None -> Flags.is_polymorphic_inductive_cumulativity ()
+	      Some true -> LocalCumulativity
+            | Some false -> LocalNonCumulativity
+	    | None ->
+                if Flags.is_polymorphic_inductive_cumulativity () then
+                  GlobalCumulativity
+                else
+                  GlobalNonCumulativity
 	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 379c83b245..e3010e3b53 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1471,7 +1471,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1486,7 +1486,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a68b569cbe..4c50c2f368 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -760,7 +760,11 @@ open Decl_kinds
                        | Class _ -> "Class" | Variant -> "Variant"
           in
           if p then
-            let cm = if cum then "Cumulative" else "NonCumulative" in
+            let cm =
+              match cum with
+              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
+              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+            in
             cm ^ " " ^ kind
           else kind
         in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 12a31953c5..1556beb060 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,12 +522,21 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
-let check_cumulativity_polymorphism_flag cum poly =
-  if cum && not poly then 
-    user_err Pp.(str "Monomorphic cumulative inductive types/records are not supported. ")
+let should_treat_as_cumulative cum poly =
+  if poly then
+    match cum with
+    | GlobalCumulativity | LocalCumulativity -> true
+    | GlobalNonCumulativity | LocalNonCumulativity -> false
+  else
+    match cum with
+    | GlobalCumulativity | GlobalNonCumulativity -> false
+    | LocalCumulativity -> 
+      user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+    | LocalNonCumulativity ->
+      user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
 
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
-  check_cumulativity_polymorphism_flag cum poly;
+  let is_cumulative = should_treat_as_cumulative cum poly in
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -538,14 +547,14 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort))
+    ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
 
 (** When [poly] is true the type is declared polymorphic. When [lo] is true,
     then the type is declared private (as per the [Private] keyword). [finite]
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive cum poly lo finite indl =
-  check_cumulativity_polymorphism_flag cum poly;
+  let is_cumulative = should_treat_as_cumulative cum poly in
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -582,7 +591,7 @@ let vernac_inductive cum poly lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl cum poly lo finite
+    do_mutual_inductive indl is_cumulative poly lo finite
 
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
-- 
cgit v1.2.3


From 819fd4a7a431efb41a080e7aabef2a66a3ca2417 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Mon, 31 Jul 2017 11:50:54 +0200
Subject: Update documentation of cumulativity

---
 doc/refman/Universes.tex | 45 ++++++++++++++++++++-------------------------
 1 file changed, 20 insertions(+), 25 deletions(-)

diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index e097de59b3..667fd66984 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -134,12 +134,12 @@ producing global universe constraints, one can use the
 \asection{{\tt Cumulative, NonCumulative}}
 \comindex{Cumulative}
 \comindex{NonCumulative}
-\optindex{Inductive Cumulativity}
+\optindex{Polymorphic Inductive Cumulativity}
 
-Inductive types, coinductive types, variants and records can be
+Polymorphic inductive types, coinductive types, variants and records can be
 declared cumulative using the \texttt{Cumulative}. Alternatively,
-there is an option \texttt{Set Inductive Cumulativity} which when set,
-makes all subsequent inductive definitions cumulative.  When set,
+there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
+makes all subsequent \emph{polymorphic} inductive definitions cumulative.  When set,
 inductive types and the like can be enforced to be
 \emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below.
 \begin{coq_example*}
@@ -160,15 +160,6 @@ This also means that any two instances of \texttt{list} are convertible:
 $\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
 furthermore their corresponding (when fully applied to convertible arguments) constructors.
 See Chapter~\ref{Cic} for more details on convertibility and subtyping.
-Also notice the subtyping constraints for the \emph{non-cumulative} version of list:
-\begin{coq_example*}
-Polymorphic NonCumulative Inductive list' {A : Type} :=
-| nil' : list'
-| cons' : A -> list' -> list'.
-\end{coq_example*}
-\begin{coq_example}
-Print list'.
-\end{coq_example}
 The following is an example of a record with non-trivial subtyping relation:
 \begin{coq_example*}
 Polymorphic Cumulative Record packType := {pk : Type}.
@@ -176,33 +167,37 @@ Polymorphic Cumulative Record packType := {pk : Type}.
 \begin{coq_example}
 Print packType.
 \end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}.
+Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
+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 inputs such a monomorphic and
-cumulative type. Notice that this also implies that when the option
-\texttt{Set Inductive Cumulativity} is set any subsequent inductive
-declaration should be polymorphic, e.g., by setting \texttt{Set
-  Universe Polymorphism}, unless it is specifically made
-\emph{non-cumulative} using the \texttt{NonCumulative} prefix.
-
+error is issued whenever the user uses the \texttt{Cumulative} or
+\texttt{NonCumulative} prefix in a monomorphic contexts.
+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)
+but has no effect on \emph{monomorphic} inductive declarations.
+Consider the following examples.
 \begin{coq_example}
 Fail Monomorphic Cumulative Inductive Unit := unit.
 \end{coq_example}
 \begin{coq_example}
-Set Inductive Cumulativity.
-Fail Inductive Unit := unit.
+Fail Monomorphic NonCumulative Inductive Unit := unit.
 \end{coq_example}
+\begin{coq_example*}
+Set Polymorphic Inductive Cumulativity.
+Inductive Unit := unit.
+\end{coq_example*}
 \begin{coq_example}
-NonCumulative Inductive Unit := unit.
+Print Unit.
 \end{coq_example}
 
 \subsection*{An example of a proof using cumulativity}
 
 \begin{coq_example}
 Set Universe Polymorphism.
-Set Inductive Cumulativity.
+Set Polymorphic Inductive Cumulativity.
 
 Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
 
-- 
cgit v1.2.3


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