diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
2 files changed, 15 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst new file mode 100644 index 0000000000..b105928b22 --- /dev/null +++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 <https://github.com/coq/coq/pull/11530>`_, + by Hugo Herbelin, fixing in particular + `#9517 <https://github.com/coq/coq/pull/9517>`_, + `#9519 <https://github.com/coq/coq/pull/9519>`_, + `#9521 <https://github.com/coq/coq/pull/9521>`_, + `#11331 <https://github.com/coq/coq/pull/11331>`_). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..a8d5ac610f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to |