1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 466b4cde5..eaceea6da 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
 
@@ -110,6 +112,8 @@ Standard Library
   Coq.Numbers.DecimalString providing a type of decimal numbers, some
   facts about them, and conversions between decimal numbers and nat,
   positive, N, Z, and string.
+- Added [Coq.Strings.String.concat] to concatenate a list of strings
+  inserting a separator between each item
 
 - Some deprecated aliases are now emitting warnings when used.