diff options
| author | Hugo Herbelin | 2020-08-31 20:27:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 23:29:14 +0200 |
| commit | 899e3cd4bba5c6ba0ec6ec60f20acf4ae507fa27 (patch) | |
| tree | e65e0463b8ec81e4a2058f85c3e539a249be0f9b | |
| parent | d680b80092861b0c10e220cdf8d91e8ae35c0252 (diff) | |
Adding change log for #12960.
| -rw-r--r-- | doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst new file mode 100644 index 0000000000..fc909e7a1d --- /dev/null +++ b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 <https://github.com/coq/coq/pull/12960>`_, + fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ + and `#10803 <https://github.com/coq/coq/issues/10803>`_, + by Hugo Herbelin). |