diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25336be82f3f7c32e4d8e1f87ee932a468124fb0..0749a2fd8f1d05540834379b3e48bd9d1f07d686 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -58,10 +58,11 @@ lemma.
 * Rename `head_step` to `base_step` to avoid potential confusion with the
   standard term "head reduction", and also rename all associated definitions and
   lemmas. In particular: `head_stuck` → `base_stuck`, `head_reducible` →
-  `base_reducible`, `head_irreducible` → `base_irreducible`.
-  The sed script will rename all definitions and lemmas that come with Iris,
-  but if you had additional definitions or lemmas with `head` in their name,
-  you will have to rename them by hand if you want to remain consistent.
+  `base_reducible`, `head_irreducible` → `base_irreducible`, `head_redex` →
+  `base_redex`, `head_atomc` → `base_atomic`. The sed script will rename all
+  definitions and lemmas that come with Iris, but if you had additional
+  definitions or lemmas with `head` in their name, you will have to rename them
+  by hand if you want to remain consistent.
 
 **Changes in `heap_lang`:**