From a0090dc6930c1f0c60ca6144d1551019ecbcc837 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 30 Aug 2020 07:58:06 +0200
Subject: Adding change log for #12946.

---
 ...946-master+fix12908-part1-collision-lonely-notation-printing.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst

(limited to 'doc')

diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst
new file mode 100644
index 0000000000..95a9093272
--- /dev/null
+++ b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Undetected collision between a lonely notation and a notation in
+  scope at printing time
+  (`#12946 <https://github.com/coq/coq/pull/12946>`_,
+  fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3