diff options
| author | Hugo Herbelin | 2019-12-21 20:03:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-21 20:03:49 +0100 |
| commit | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (patch) | |
| tree | c144c0aa94dd4392e165c8780b7e1883fea95fcb /doc | |
| parent | a325c1b8a2e901a369793805a44487e3468c4348 (diff) | |
| parent | 515bdf52963c42f007178b608d8dc0707b340360 (diff) | |
Merge PR #11311: Fix handling of recursive notations with custom entries
Reviewed-by: herbelin
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>`_). |