diff options
| author | Enrico Tassi | 2019-06-07 10:00:21 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-07 10:04:23 +0200 |
| commit | cbba70dde9ce6427560d267680f6a69fb97349a2 (patch) | |
| tree | aeac006c1718dcaf7557097456aa315586893150 | |
| parent | 32f965d53d7e0f969af5f9c52adc5cf7bd2a97a3 (diff) | |
Update changelog for 103032 and 10305
| -rw-r--r-- | doc/changelog/06-ssreflect/10302-case-HoTT.rst | 7 | ||||
| -rw-r--r-- | doc/changelog/06-ssreflect/10305-unfold-HoTT.rst | 7 |
2 files changed, 14 insertions, 0 deletions
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) |