diff options
| author | Erik Martin-Dorel | 2019-06-26 00:44:53 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-06-26 00:54:13 +0200 |
| commit | 5fc787004d260051100ed28c061671680387b037 (patch) | |
| tree | d29c75c86b26b85607eb7243a403114bb6c2679c /CHANGELOG.md | |
| parent | 19f1ace7d69b7d63af3626c695a3e1e917f35e30 (diff) | |
docs: Add missing entry in CHANGELOG.md
href: math-comp/math-comp#292
Diffstat (limited to 'CHANGELOG.md')
| -rw-r--r-- | CHANGELOG.md | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index 30fcd0f..f8c3221 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -119,6 +119,10 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. with its theory: `mem_permutations`, `size_permutations`, `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`. +- `eq_mktuple`, `eq_ffun`, `eq_finset`, `eq_poly`, `ex_mx` that can be + used with the `under` tactic from the Coq 8.10 SSReflect plugin + (cf. [coq/coq#9651](https://github.com/coq/coq/pull/9651)) + ### Changed - Theory of `lersif` and intervals: |