changelog

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`:**