diff options
Diffstat (limited to 'doc/changelog/03-notations/11120-master+refactoring-application-printing.rst')
| -rw-r--r-- | doc/changelog/03-notations/11120-master+refactoring-application-printing.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst index d95f554766..eeb4c755f6 100644 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -10,7 +10,7 @@ Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and `#11091 <https://github.com/coq/coq/pull/11091>`_). -- **Changed:** Interpretation scopes are now always inherited in +- **Changed:** Notation scopes are now always inherited in notations binding a partially applied constant, including for notations binding an expression of the form :n:`@@qualid`. The latter was not the case beforehand |