1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 81d1a59e2..78edfd6e2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,7 @@ Language
 
 - Inductive definitions now accept ">" in constructor types to declare
   the corresponding constructor as a coercion.
+- Idem for assumptions declarations and constants when the type is mentionned.
 
 ML tactic and vernacular commands