diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e52259f4a6bd8c20c056964477e7493f848157..913a7e5d873db5e4ebaf78ac04993eaaa1f3359e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -37,6 +37,22 @@ Coq 8.12 and 8.13 are no longer supported by this release.
   Lesbre)
 - Add proof that `vec` is `Finite`. (by Herman Bergwerf.)
 - Add `min` and `max` infix notations for `positive`.
+- Provide new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
+  `Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
+  Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma
+  types and enjoy:
+  + More definitional equalities, because maps are no longer equipped with a
+    proof of canonicity. This means more equalities can be proved by
+    `reflexivity` or even by conversion as part of unification. For example,
+    `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}` and `{[ 1 ]} ∖ {[ 1 ]} = ∅`
+    hold definitionally.
+  + The use in nested recursive definitions. For example,
+    `Inductive gtest := GTest : gmap nat gtest → gtest`. (The old map types
+    would violate Coq's strict positivity condition due to the Sigma type.)
+- Make `map_fold` a primitive of the `FinMap`, and derive `map_to_list` from it.
+  (Before `map_fold` was derived from `map_to_list`.) This makes it possible to
+  use `map_fold` in nested-recursive definitions on maps. For example,
+  `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).