diff options
| author | Théo Zimmermann | 2020-12-10 11:20:50 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-12-10 21:27:20 +0100 |
| commit | 1e37c5234f3237eeb7fef85d461e6b8108cd0edf (patch) | |
| tree | 70851d8478ec92733142f71709ae0abfc31d3895 /doc | |
| parent | 358e923ea477fff4ffe9ebac9c1910a65afe9e90 (diff) | |
Changelog for 8.12.2.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/changes.rst | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 8fb03879e8..726a6309d4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2017,6 +2017,25 @@ Changes in 8.12.1 fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, by Théo Zimmermann and Jim Fehrle). +Changes in 8.12.2 +~~~~~~~~~~~~~~~~~ + +**Notations** + +- **Fixed:** + 8.12 regression causing notations mentioning a coercion to be ignored + (`#13436 <https://github.com/coq/coq/pull/13436>`_, + fixes `#13432 <https://github.com/coq/coq/issues/13432>`_, + by Hugo Herbelin). + +**Tactics** + +- **Fixed:** + 8.12 regression: incomplete inference of implicit arguments in :tacn:`exists` + (`#13468 <https://github.com/coq/coq/pull/13468>`_, + fixes `#13456 <https://github.com/coq/coq/issues/13456>`_, + by Hugo Herbelin). + Version 8.11 ------------ |