From 9468bcd39808f4587d3732f46773b1e339b2267c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Jul 2016 15:26:28 +0200
Subject: Update CHANGES, the bugfixes for 4527 and 4726 are

not in pl2.
---
 CHANGES | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index 37abece248..1de3c25d84 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,14 @@
 Changes beyond V8.5
 ===================
+Bugfixes
+
+- #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).
+- #4726: treat user-provided sorts of universe polymorphic records as rigid
+  (i.e. non-minimizable).
 
 Specification language
 
@@ -81,13 +90,6 @@ 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).
-- #4726: treat user-provided sorts of universe polymorphic records as rigid
-  (i.e. non-minimizable).
 
 Changes from V8.5 to V8.5pl1
 ============================
-- 
cgit v1.2.3