1 files changed, 6 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index fa0e70ba0a..db27f82001 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes beyond V8.5
 ===================
 
+Specification language
+
+- Giving implicit arguments explicitly to a constant with multiple
+  choices of implicit arguments does not break any more insertion of
+  further maximal implicit arguments.
+
 Tactics
 
 - Flag "Bracketing Last Introduction Pattern" is now on by default.