diff options
| author | Théo Zimmermann | 2019-06-12 14:07:49 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-12 14:07:49 +0200 |
| commit | 288f567897a8af92a4a0c78c63a433b6f64af0d0 (patch) | |
| tree | 2b76fbf6615b8ec38f1961e4ae1556c2f803d44c | |
| parent | 0ab76e968b9f3a02678ec8aa747da47f94181055 (diff) | |
| parent | cbba70dde9ce6427560d267680f6a69fb97349a2 (diff) | |
Merge PR #10329: Update changelog for 10302 and 10305
Reviewed-by: Zimmi48
| -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) |