diff options
| author | Cyril Cohen | 2019-06-26 13:31:13 +0200 |
|---|---|---|
| committer | GitHub | 2019-06-26 13:31:13 +0200 |
| commit | 1bda1dd5621684737c9d993855ae104e8b9d2909 (patch) | |
| tree | d29c75c86b26b85607eb7243a403114bb6c2679c | |
| parent | 19f1ace7d69b7d63af3626c695a3e1e917f35e30 (diff) | |
| parent | 5fc787004d260051100ed28c061671680387b037 (diff) | |
Merge pull request #364 from erikmd/update/changelog
docs: Add missing entry in CHANGELOG.md regarding #292
| -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: |