Document cumulativity for inductive types

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b5aaad725..deca62f92 100644
--- a/CHANGES
+++ b/CHANGES
@@ -94,6 +94,12 @@ Build Infrastructure
   access to the same .cmi files. In short, use "make -j && make -j byte"
   instead of "make -j world byte".
 
+Universes
+
+- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative"
+  for inductive definitions and the option "Set Inductive Cumulativity"
+  in the reference manual.
+
 Changes from V8.6beta1 to V8.6
 ==============================