blob: d95f5547663e70446a00c72fa6f6dc4e84334d1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
- **Fixed:** Parsing and printing consistently handle inheritance of implicit
arguments in notations. With the exception of notations of
the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
inhibit implicit arguments, all notations binding a partially
applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
or :n:`Notation @string := (@@qualid {+ @arg })`, or
:n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
:= (@@qualid {+ @arg })`, inherit the remaining implicit arguments
(`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
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
notations binding a partially applied constant, including for
notations binding an expression of the form :n:`@@qualid`. The latter was
not the case beforehand
(part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
|
