diff options
| author | Vincent Laporte | 2019-10-06 13:26:09 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-06 13:26:09 +0000 |
| commit | 8ecc5555b1b79ec2278cd9d425dab6c209139c3a (patch) | |
| tree | 80aa8c4d7bb6889e7f63ebc0a4b2ecb995966391 /doc | |
| parent | 97a2047d32aa1dc8689ff65eff5f82a6efa74656 (diff) | |
| parent | ee4ee17d86ddb11a6508335b9e5d5792bcdf6a8a (diff) | |
Merge PR #10833: 8.10.0 release notes.
Reviewed-by: vbgl
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 ----------- |