Adding changelog for coq#17856

herbelin · Nov 16, 2023 · 16b0e80 · 16b0e80
1 parent 5e2a7c1
commit 16b0e80
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/...elog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst b/...elog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Parsing support for notations with recursive binders involving not only
+  variables bound by :n:`fun` or :n:`forall` but also by :n:`let` or
+  :n:`match`
+  (`#17856 <https://github.com/coq/coq/pull/17856>`_,
+  fixes `#17845 <https://github.com/coq/coq/issues/17845>`_,
+  by Hugo Herbelin).