diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 8 |
2 files changed, 8 insertions, 4 deletions
diff --git a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst deleted file mode 100644 index d6fc724415..0000000000 --- a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst +++ /dev/null @@ -1,4 +0,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). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 38b3c34209..0148925247 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -718,6 +718,14 @@ 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). + Version 8.9 ----------- |