diff options
| author | coqbot-app[bot] | 2020-12-10 20:48:34 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-10 20:48:34 +0000 |
| commit | 1918f19cb43d6d4313276b167af38316b27879f2 (patch) | |
| tree | cb0865c7332ca5174e1b8cb01cb506ab12463717 | |
| parent | 71031ef2a7032bccb55cc0e6035900c5b843583c (diff) | |
| parent | 1e37c5234f3237eeb7fef85d461e6b8108cd0edf (diff) | |
Merge PR #13608: Changelog for 8.12.2.
Reviewed-by: jfehrle
| -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 ------------ |