From d1fe597eee63caccd50d4a6da529856f295872be Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2020 15:21:29 +0100
Subject: [kernel] Fix #13495: incompleteness in cases typing for cumulative
 inductive types

---
 doc/changelog/01-kernel/13501-fix-13495.rst | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 doc/changelog/01-kernel/13501-fix-13495.rst

(limited to 'doc')

diff --git a/doc/changelog/01-kernel/13501-fix-13495.rst b/doc/changelog/01-kernel/13501-fix-13495.rst
new file mode 100644
index 0000000000..5c81efa8b9
--- /dev/null
+++ b/doc/changelog/01-kernel/13501-fix-13495.rst
@@ -0,0 +1,7 @@
+- **Fixed:**
+  Fix an incompleteness in the typechecking of `match` for
+  cumulative inductive types. This could result in breaking subject
+  reduction.
+  (`#13501 <https://github.com/coq/coq/pull/13501>`_,
+  fixes `#13495 <https://github.com/coq/coq/issues/13495>`_,
+  by Matthieu Sozeau).
-- 
cgit v1.2.3