1 files changed, 2 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 85117132d2..ed2f172067 100644
--- a/CHANGES
+++ b/CHANGES
@@ -158,7 +158,8 @@ Universes
 - Cumulative inductive types. see prefixes "Cumulative", "NonCumulative"
   for inductive definitions and the option "Set Inductive Cumulativity"
   in the reference manual.
-- New syntax `Type@{_}` for anonymous universes.
+- New syntax `foo@{_}` to instantiate a polymorphic definition with
+  anonymous universes (can also be used with `Type`).
 
 XML Protocol and internal changes