From b0708b013c473cd0e7b608329c11ad4659bb22e1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 6 Mar 2021 13:46:49 +0100
Subject: [PATCH] fixup changelog

---
 CHANGELOG.md | 30 +++++++++++++-----------------
 1 file changed, 13 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8661be2f8..72b73b157 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,22 +17,6 @@ lemma.
 
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
   view and per-element points-to facts written `k ↪[γ] w`.
-
-The following `sed` script helps adjust your code to the renaming (on macOS,
-replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-Note that the script is not idempotent, do not run it twice.
-```
-sed -i -E -f- $(find theories -name "*.v") <<EOF
-# auth and view renames from frac to dfrac
-s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
-s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
-s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
-s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
-EOF
-```
-
-**Changes in `base_logic`:**
-
 * Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
   It applies even if invariants stay open accross an arbitrary number of laters.
 
@@ -42,7 +26,6 @@ EOF
   (i.e., logical steps) for each physical step of the operational semantics,
   depending on the number of physical steps executed since the begining of the
   execution of the program. See merge request [!595](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595).
-
   This implies several API-breaking changes, which can be easily fixed in client
   formalizations in a backward compatible manner as follows:
    - Ignore the new parameter `ns` in the state interpretation, which
@@ -53,6 +36,19 @@ EOF
    - Some proofs using lifting lemmas and adequacy theorems need to be adapted
      to ignore the new step counter.
 
+The following `sed` script helps adjust your code to the renaming (on macOS,
+replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# auth and view renames from frac to dfrac
+s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
+s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
+s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
+s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
+EOF
+```
+
 ## Iris 3.4.0
 
 The highlights and most notable changes of this release are as follows:
-- 
GitLab