diff --git a/CHANGELOG.md b/CHANGELOG.md
index 91836201893e036a9063112abb56290a84023458..36f0f1301c92a2414317d374cd52944d5c726367 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -22,6 +22,13 @@ API-breaking change is listed.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
 - Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
 - Add `option_guard_True_pi`.
+- Add lemma `surjective_finite` (by Alix Trieu).
+- Add type classes `TCFalse`, `TCUnless`, `TCExists`, and `TCFastDone` (by
+  Michael Sammler).
+- Add various results about bit representations of `Z` (by Michael Sammler).
+- Add tactic `learn_hyp` (by Michael Sammler).
+- Add `Countable` instance for decidable Sigma types (by Simon Gregersen).
+- Add tactics `compute_done` and `compute_by` for solving goals by computation.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):