From 7b8ed629b2e05dc9a71ce1c62e075adeecae16f3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 20:01:03 +0100
Subject: Adding overlay for PR #13290.

---
 .../13290-master+grant13278-small-inversion-in-prop.rst             | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst

(limited to 'doc')

diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst
new file mode 100644
index 0000000000..bf792fda6d
--- /dev/null
+++ b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Inference of return predicate of a :g:`match` by inversion takes
+  sort elimination constraints into account
+  (`#13290 <https://github.com/coq/coq/pull/13290>`_,
+  grants `#13278 <https://github.com/coq/coq/issues/13278>`_,
+  by Hugo Herbelin).
-- 
cgit v1.2.3