From ebbc65955f1fa65965fd90a23b862fd629a23f73 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Feb 2018 11:03:13 +0100
Subject: CHANGES for universe variance

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index cb4b966b08..1084847d52 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
 
-- 
cgit v1.2.3