CHANGES and tests for with Definition @{univs}

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 466b4cde5..ab6aab0ee 100644
--- a/CHANGES
+++ b/CHANGES
@@ -86,6 +86,8 @@ Universes
   more information.
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
+- `with Definition` now understands universe declarations
+  (like `@{u| Set < u}`).
 
 Checker