diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d11d393074660c6864f4e013ad6b97bb81b1b56..59ed387aef40f42bfd6c9dc39b562a41d8badd8a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,8 @@ With this release, we dropped support for Coq 8.9.
 * Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
   That module is exported by `base_logic.base_logic` so it should usually be
   available everywhere without further changes.
+* The authoritative fragment `✓ (◯ b : auth A)` is no longer definitionally
+  equal to `✓ b`.
 
 **Changes in `proofmode`:**