diff --git a/CHANGELOG.md b/CHANGELOG.md
index 518d58d5d46c76f3f6e8517934b74c3fb3f0c648..ac6566191319dfe3d556f19ae414a389527df9d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,7 @@ lemma.
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
 * `iInduction` now supports induction schemes that involve `Forall` and
   `Forall2` (for example, for trees with finite branching).
+* `iRevert` of a pure hypothesis generates a wand instead of an implication.
 
 **Changes in `base_logic`:**