From c3aae082aa12d3e5b338888193cbb0a01d9ca7e5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Mar 2021 00:11:43 +0100
Subject: [PATCH] fix changelog order

---
 CHANGELOG.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index de0d390c2..3ac18c6dd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -25,6 +25,12 @@ lemma.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 
+**Changes in `proof_mode`:**
+
+* Add support for pure names `%H` in intro patterns. This is now natively
+  supported whereas the previous experimental support required installing
+  https://gitlab.mpi-sws.org/iris/string-ident.
+
 **Changes in `base_logic`:**
 
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
@@ -52,12 +58,6 @@ lemma.
 
 * Rename `Build_loc` constructor for `loc` type to `Loc`.
 
-**Changes in `proof_mode`:**
-
-* Add support for pure names `%H` in intro patterns. This is now natively
-  supported whereas the previous experimental support required installing
-  https://gitlab.mpi-sws.org/iris/string-ident.
-
 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.
-- 
GitLab