From 23ab6c84b3d04cc2218bf1ad935fa87396999ccd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 9 Jun 2016 15:40:28 +0200
Subject: CHANGES: document fix for #4726 too.

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

diff --git a/CHANGES b/CHANGES
index 4d9d451c4..4808dee79 100644
--- a/CHANGES
+++ b/CHANGES
@@ -85,6 +85,8 @@ Bugfixes
   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