From 6de02170275e49e5f58a93eb5513d5eb8cb9aa38 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 17 Aug 2017 15:35:49 +0200
Subject: Use the wording suggested by Gaetan.

---
 CHANGES | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3