diff --git a/CHANGELOG.md b/CHANGELOG.md
index cd33b885352b49fd6cd69575593aa2b1d33623f3..e926aad99efc4141c103ad5bd532df24a14c6b03 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,7 @@ Coq 8.13 is no longer supported.
     particular, replace `apply` by `iApply`).
   - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
     between the old and new way of interpreting `P -∗ Q`.
+* Add `auto` hint to introduce the BI version of `↔`.
 
 **Changes in `proofmode`:**