diff --git a/CHANGELOG.md b/CHANGELOG.md
index c655bd855c70f1872aecd978c4c5742129cf06c1..c0a929796b4adee2ca3c60b9c93eac1ddac57986 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -86,6 +86,11 @@ Coq 8.13 is no longer supported.
     `Fractional`, making it very hard to reason about search termination).
   - Rewrite `frame_fractional` lemma using the new `FrameFractionalQp` typeclass
     for `Qp` reasoning.
+  - Change statements of `fractional_split`, `fractional_half`, and
+    `fractional_merge` to avoid using `AsFractional` backwards, and only keep
+    the bi-directional versions (remove `fractional_split_1`,
+    `fractional_split_2`, `fractional_half_1`, `fractional_half_2`).
+    `iDestruct`/`iCombine`/`iSplitL`/`iSplitR` should be used instead.
 * Add missing transitivity, symmetry and reflexivity lemmas about the `↔`, `→`,
   `-∗` and `∗-∗` connectives. (by Ike Mulder)