diff options
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 77 |
1 files changed, 62 insertions, 15 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 38b3c34209..80a24b997c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -198,21 +198,21 @@ Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2) with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. -The 61 contributors to this version are David A. Dalrymple, Tanaka -Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse -Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric -Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian -Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj -Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin, -Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal -Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee -Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia -Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume -Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan -Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, -Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo -Winterhalter, Beta Ziliani and Théo Zimmermann. +The 61 contributors to this version are Tanaka Akira, Benjamin +Barenblat, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Martin +Bodin, Joachim Breitner, Tej Chajed, Frédéric Chapoton, Arthur +Charguéraud, Cyril Cohen, Lukasz Czajka, David A. Dalrymple, Christian +Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego +Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross, +Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi, +Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier +Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia +Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, +Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot, +Clément Pit-Claudel, Pierre Roux, Kazuhiko Sakaguchi, Ryan Scott, +Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo Winterhalter, +Xia Li-yao, Beta Ziliani and Théo Zimmermann. Many power users helped to improve the design of the new features via the issue and pull request system, the |Coq| development mailing list, @@ -718,6 +718,53 @@ Changes in 8.10+beta3 follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_, which added ``uncons`` in 8.10+beta1). +Changes in 8.10.0 +~~~~~~~~~~~~~~~~~ + +- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by + primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_, + fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ + by Vincent Laporte). + +Changes in 8.10.1 +~~~~~~~~~~~~~~~~~ + +A few bug fixes and documentation improvements, in particular: + +**Kernel** + +- Fix proof of False when using |SProp| (incorrect De Bruijn handling + when inferring the relevance mark of a function) (`#10904 + <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). + +**Tactics** + +- Fix an anomaly when unsolved evar in :cmd:`Add Ring` + (`#10891 <https://github.com/coq/coq/pull/10891>`_, + fixes `#9851 <https://github.com/coq/coq/issues/9851>`_, + by Gaëtan Gilbert). + +**Tactic language** + +- Fix Ltac regression in binding free names in uconstr + (`#10899 <https://github.com/coq/coq/pull/10899>`_, + fixes `#10894 <https://github.com/coq/coq/issues/10894>`_, + by Hugo Herbelin). + +**CoqIDE** + +- Fix handling of unicode input before space + (`#10852 <https://github.com/coq/coq/pull/10852>`_, + fixes `#10842 <https://github.com/coq/coq/issues/10842>`_, + by Arthur Charguéraud). + +**Extraction** + +- Fix custom extraction of inductives to JSON + (`#10897 <https://github.com/coq/coq/pull/10897>`_, + fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, + by Helge Bahmann). + Version 8.9 ----------- |