From 16b0e80fd9e1c5c63ef52efe4c33d988ff7351bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 14 Jul 2023 11:37:32 +0200
Subject: [PATCH] Adding changelog for #17856

---
 ...master+more-general-form-binders-recursive-notation.rst | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 doc/changelog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst

diff --git a/doc/changelog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst b/doc/changelog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst
new file mode 100644
index 0000000000000..4250fd54ae2d9
--- /dev/null
+++ b/doc/changelog/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).