diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2d4c2af057b318d42d95d891c1ce9b90fda2fdfd..a3305d69634e1c382924d143fb521dd6bccb7616 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ Changes in Coq:
 
 * Rename some things and change notation:
   - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
+  - Disjointness: `⊥` -> `##`
   - A proof mode type class `IntoOp` -> `IsOp`
   - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
   - OFE elements whose equality is discrete: `Timeless` -> `Discrete`