From e783acc0ff10d76403c1c3f665e984fa7a37e9b6 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sun, 16 Jun 2019 22:39:52 +0200 Subject: Changelog for 8.10+beta2. --- doc/sphinx/changes.rst | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'doc/sphinx') diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6ff15e52a3..e5045c222a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -604,6 +604,43 @@ Other changes in 8.10+beta1 with help and ideas from Emilio Jesús Gallego Arias, Gaëtan Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). +Changes in 8.10+beta2 +~~~~~~~~~~~~~~~~~~~~~ + +Many bug fixes and documentation improvements, in particular: + +**SSReflect** + +- 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 `_, + fixes `#10301 `_, + by Andreas Lynge, review by Enrico Tassi) +- 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 `_, + fixes `#9336 `_, + by Andreas Lynge, review by Enrico Tassi) + +**CoqIDE** + +- Fix CoqIDE instability on Windows after the update to gtk3 + (`#10360 `_, by Michael Soegtrop, + closes `#9885 `_). + +**Miscellaneous** + +- Proof General can now display Coq-generated diffs between proof steps + in color + (`#10019 `_ and + (in Proof General) `#421 `_, + by Jim Fehrle). + + Version 8.9 ----------- -- cgit v1.2.3