diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8f5b09bab19f9c3629b8f2f4ee6a230294b4c433..2d4c2af057b318d42d95d891c1ce9b90fda2fdfd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -115,7 +115,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Slightly weaker notion of atomicity: an expression is atomic if it reduces in
   one step to something that does not reduce further.
 * Changed notation for embedding Coq assertions into Iris.  The new notation is
-  ⌜φ⌝.  Also removed `=` and `##` from the Iris scope.  (The old notations are
+  ⌜φ⌝.  Also removed `=` and `⊥` from the Iris scope.  (The old notations are
   provided in `base_logic.deprecated`.)
 * Up-closure of namespaces is now a notation (↑) instead of a coercion.
 * With invariants and the physical state being handled in the logic, there is no