diff options
| author | Maxime Dénès | 2019-12-19 12:45:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-20 13:27:13 +0100 |
| commit | 7149fef354d55f4b5012eac7efa15b4e7bac3d38 (patch) | |
| tree | ab27bfa6035490d65205702854d34dd16411c029 /doc | |
| parent | 5c667d56cd0a441f787019aef44bf18bec9c7b20 (diff) | |
Fix handling of recursive notations with custom entries
Fixes #9532
Fixes #9490
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>`_). |