1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index be07cfe7b9..b6744e25d3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,8 @@ Notations
 - Abbreviations now use implicit arguments and arguments scopes for printing.
 - Abbreviations to pure names now strictly behave like the name they refer to
   (make redirections of qualified names easier).
+- Abbreviations to applied names now propagate the implicit arguments and
+  arguments scope of the underlying reference.
 - The "where" clause now supports multiple notations per defined object.
 
 Vernacular commands