From 4c90b4243c49b46152eede195a086bc8dc8a86ec Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 15:36:02 +0200
Subject: CHANGES: document fix for 4527 and compatibility.

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

diff --git a/CHANGES b/CHANGES
index 9ef048345c..4d9d451c4a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -80,6 +80,11 @@ Bugfixes
 - #4777: printing inefficiency with implicit arguments
 - #4752: CoqIDE crash on files not ended by ".v".
 - #4398: type_scope used consistently in "match goal".
+- #4527: when typechecking the statement of a lemma using universe polymorphic
+  definitions with explicit universe binders, check that the type can indeed be
+  typechecked using only those universes (after minimization of the other,
+  flexible universes), or raise an error (fixed scripts can be made forward
+  compatible).
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3