aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/06-ssreflect/10302-case-HoTT.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/changelog/06-ssreflect/10302-case-HoTT.rst')
-rw-r--r--doc/changelog/06-ssreflect/10302-case-HoTT.rst7
1 files changed, 0 insertions, 7 deletions
diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst
deleted file mode 100644
index 686b3c3cca..0000000000
--- a/doc/changelog/06-ssreflect/10302-case-HoTT.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- 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)