From e9692bedfe275668aeaa244811e090c49f6df64d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2020 22:45:53 +0200
Subject: Adding change log for #8808.

---
 .../03-notations/8808-master+support-binder+term-in-abbrev.rst        | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst

(limited to 'doc')

diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
new file mode 100644
index 0000000000..e1fcfb78c4
--- /dev/null
+++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Abbreviations support arguments occurring both in term and binder position
+  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3