diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11311-custom-entries-recursive.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst new file mode 100644 index 0000000000..ae9888512d --- /dev/null +++ b/doc/changelog/03-notations/11311-custom-entries-recursive.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). |