From a460ac3e4ca7cec4333b430a0b86388ce1a8561a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Jun 2023 16:32:39 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c655bd855..c0a929796 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)
 
-- 
GitLab