1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 63900a2b76..eb906205e9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,6 +163,8 @@ Vernacular commands
   variables before the colon at the start of interactive proofs.
 - New command "Declare Reduction <id> := <conv_expr>", allowing to write
   later "Eval <id> in ...". This command accepts a Local variant.
+- Syntax of Implicit Type now supports more than one block of variables of
+  a given type.
 
 Library