From 75ae147648b8362a4a75718db8bbc57940e90c7d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 9 Sep 2020 13:07:42 +0200
Subject: changelog entry for 12857

---
 doc/changelog/06-ssreflect/12857-changelog-for-12857.rst | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 doc/changelog/06-ssreflect/12857-changelog-for-12857.rst

(limited to 'doc')

diff --git a/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst b/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst
new file mode 100644
index 0000000000..a436253e3b
--- /dev/null
+++ b/doc/changelog/06-ssreflect/12857-changelog-for-12857.rst
@@ -0,0 +1,7 @@
+- **Fixed:**
+  Regression in error reporting after tacn:`case`.
+  A generic error message "Could not fill dependent hole in apply"" was
+  reported for any error following tacn:`case` or tacn:`elim`
+  (`#12857 <https://github.com/coq/coq/pull/12857>`_,
+  fixes `#12837 <https://github.com/coq/coq/issues/12837>`_,
+  by Enrico Tassi).
-- 
cgit v1.2.3