Merge PR #6738: CHANGES for universe variance

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index cb4b966b0..1084847d5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,9 @@ Universes
   module and library boundaries. Global universe names introduced in an
   inductive / constant / Let declaration get qualified with the name of
   the declaration.
+- Universe cumulativity for inductive types is now specified as a
+  variance for each polymorphic universe. See the reference manual for
+  more information.
 
 Checker