CHANGES: document fix for #4726 too.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4d9d451c4a..4808dee794 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
 ============================