From 416cccb2b0c7db284130723ef1c2f3851b995ae9 Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Tue, 21 May 2019 20:37:42 +0200
Subject: Make discriminate tactic compatible with HoTT

---
 doc/changelog/04-tactics/10205-discriminate-HoTT.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/04-tactics/10205-discriminate-HoTT.rst

(limited to 'doc')

diff --git a/doc/changelog/04-tactics/10205-discriminate-HoTT.rst b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst
new file mode 100644
index 0000000000..bb2d2a092e
--- /dev/null
+++ b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst
@@ -0,0 +1,6 @@
+- Make the :tacn:`discriminate` tactic work together with
+  :flag:`Universe Polymorphism` and equality in :g:`Type`. This,
+  in particular, makes :tacn:`discriminate` compatible with the HoTT
+  library https://github.com/HoTT/HoTT.
+  (`#10205 <https://github.com/coq/coq/pull/10205>`_,
+  by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau)
-- 
cgit v1.2.3