diff --git a/CHANGELOG.md b/CHANGELOG.md
index c91ae4838a92b818a5b61c4f2c7263eaae58409b..5eb8ef8e36c1675ed6fcc526e7b615409f964665 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,6 +14,7 @@ Coq 8.13 is no longer supported.
   lemmas using `=` instead of `<->`.
 * Add custom entry `dfrac` that can be used for `{dq}` / `â–¡` / `{# q}`
   annotation of connectives with a discardable fraction.
+* Add an RA on the `Z` type of integers, using addition for `â‹…`.
 
 **Changes in `bi`:**