From cbba70dde9ce6427560d267680f6a69fb97349a2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 7 Jun 2019 10:00:21 +0200
Subject: Update changelog for 103032 and 10305

---
 doc/changelog/06-ssreflect/10302-case-HoTT.rst   | 7 +++++++
 doc/changelog/06-ssreflect/10305-unfold-HoTT.rst | 7 +++++++
 2 files changed, 14 insertions(+)
 create mode 100644 doc/changelog/06-ssreflect/10302-case-HoTT.rst
 create mode 100644 doc/changelog/06-ssreflect/10305-unfold-HoTT.rst

diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
new file mode 100644
index 0000000000..686b3c3cca
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
@@ -0,0 +1,7 @@
+- Make the ``case E: t`` tactic work together with
+  :flag:`Universe Polymorphism` and equality in :g:`Type`.
+  This makes tacn:`case` compatible with the HoTT
+  library https://github.com/HoTT/HoTT.
+  (`#10302 <https://github.com/coq/coq/pull/10302>`_,
+  fixes `#10301 <https://github.com/coq/coq/issues/10301>`_,
+  by Andreas Lynge, review by Enrico Tassi)
diff --git a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst
new file mode 100644
index 0000000000..b82de1a879
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst
@@ -0,0 +1,7 @@
+- Make the ``rewrite /t`` tactic work together with
+  :flag:`Universe Polymorphism`.
+  This makes tacn:`rewrite` compatible with the HoTT
+  library https://github.com/HoTT/HoTT.
+  (`#10305 <https://github.com/coq/coq/pull/10305>`_,
+  fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
+  by Andreas Lynge, review by Enrico Tassi)
-- 
cgit v1.2.3