diff options
| author | Hugo Herbelin | 2020-01-02 20:02:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | acde8140bd51be112be33ae07db68b2f3b93302c (patch) | |
| tree | c9d97f3b7dae81053ccfee7631aa00ac869ebfa1 /doc | |
| parent | 9970ee1b131cb7e3b891d8258e492caafca46158 (diff) | |
Adding change log.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst | 8 |
1 files changed, 8 insertions, 0 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>`_). |