Merge PR #6775: Allow using cumulativity without forcing strict constraints.

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 25a519f159..63913bff5d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -95,6 +95,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