Experiment propagation of implicit arguments and arguments scope for

abbreviations of applied references.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12506 85f007b7-540e-0410-9357-904b9bb8a0f7

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