diff --git a/CHANGELOG.md b/CHANGELOG.md
index de0d390c2cb216b420f0e832d7b74d4711a97836..3ac18c6dd9db4fe9e924df24fff66804de0cd492 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,12 @@ lemma.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 
+**Changes in `proof_mode`:**
+
+* Add support for pure names `%H` in intro patterns. This is now natively
+  supported whereas the previous experimental support required installing
+  https://gitlab.mpi-sws.org/iris/string-ident.
+
 **Changes in `base_logic`:**
 
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
@@ -52,12 +58,6 @@ lemma.
 
 * Rename `Build_loc` constructor for `loc` type to `Loc`.
 
-**Changes in `proof_mode`:**
-
-* Add support for pure names `%H` in intro patterns. This is now natively
-  supported whereas the previous experimental support required installing
-  https://gitlab.mpi-sws.org/iris/string-ident.
-
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
 Note that the script is not idempotent, do not run it twice.