diff options
| author | Cyril Cohen | 2019-04-08 14:22:06 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-08 14:22:06 +0200 |
| commit | 10f14cf5b5e0e2ea0e84f8f981609d6c39a296cb (patch) | |
| tree | 14f6b0232f94009269ce91c04c1a841b0899b731 | |
| parent | 86d0a640383d6039302b9126620d0bf031a2a011 (diff) | |
Update CHANGELOG.md
| -rw-r--r-- | CHANGELOG.md | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index 3ea6b8c..c734df9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3,7 +3,7 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). -## [Unreleased] +## [1.8.0] - 2019-04-08 Drop compatibility with Coq 8.6 (OCaml plugin removed). MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. @@ -64,7 +64,7 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. + `countalg` goes from the field to the algebra package + `finalg` inherits from countalg + `closed_field` contains the construction of algebraic closure - for countable fields that used to be in countalg. + for countable fields that used to be in the file `countalg`. - Maximal implicits applied to reflection, injectivity and cancellation lemmas so that they are easier to pass to combinator lemmas such as @@ -123,6 +123,8 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. - Many corrections in implicits declarations. +- fixed missing joins in `ssralg`, `ssrnum`, `finalg` and `countalg` + ### Renamed Renamings also involve the `_in` suffix counterpart when applicable |