From af5eded304b74fa0fccb35a7dc284c46a96ba5cc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 6 Mar 2018 13:36:47 +0100
Subject: Documentation for Cumulativity Weak Constraints.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a514f5934c..ef94fde567 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,10 @@ Universes
 - Universe cumulativity for inductive types is now specified as a
   variance for each polymorphic universe. See the reference manual for
   more information.
+- Inference of universe constraints with cumulative inductive types
+  produces more general constraints. Unsetting new option Cumulativity
+  Weak Constraints produces even more general constraints (but may
+  produce too many universes to be practical).
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
 - `with Definition` now understands universe declarations
-- 
cgit v1.2.3