1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index cb4b966b08..1c4d8a194c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,8 @@ Universes
   module and library boundaries. Global universe names introduced in an
   inductive / constant / Let declaration get qualified with the name of
   the declaration.
+- Fix #5726: Notations that start with `Type` now support universe instances
+  with `@{u}`.
 
 Checker