Adding changelog for #17856

doc/changelog/03-notations/17856-master+more-general-form-binders-recursive-notation.rst

@@ -0,0 +1,7 @@
+- **Added:**
+  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).