CHANGES: document fix for 4527 and compatibility.

1 files changed, 5 insertions, 0 deletions

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
 ============================