From 5fc787004d260051100ed28c061671680387b037 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 26 Jun 2019 00:44:53 +0200
Subject: docs: Add missing entry in CHANGELOG.md

href: math-comp/math-comp#292
---
 CHANGELOG.md | 4 ++++
 1 file changed, 4 insertions(+)

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:
-- 
cgit v1.2.3