Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 1084847d52..545925026c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -71,6 +71,8 @@ Universes
 - Universe cumulativity for inductive types is now specified as a
   variance for each polymorphic universe. See the reference manual for
   more information.
+- Fix #5726: Notations that start with `Type` now support universe instances
+  with `@{u}`.
 
 Checker