From 287d6888c92cf879e1e5faefdb53f4c2e0ce4078 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Nov 2020 17:03:47 +0100
Subject: [PATCH] fix changelog section ordering

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4f09c95a8..897889c3b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,11 @@ With this release, we dropped support for Coq 8.9.
 * Add `mnat_auth`, a wrapper for `auth max_nat`. The result is an authoritative
   `nat` where a fragment is a lower bound whose ownership is persistent.
 
+**Changes in `bi`:**
+
+* Add big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall` and
+  `big_sepL2_forall`, `big_sepMS_forall`, `big_sepMS_impl`, and `big_sepMS_dup`.
+
 **Changes in `proofmode`:**
 
 * The proofmode now preserves user-supplied names for existentials when using
@@ -80,11 +85,6 @@ With this release, we dropped support for Coq 8.9.
   interface and factor it into a type class `BiPureForall`.
 * Add notation `¬ P` for `P → False` to `bi_scope`.
 
-**Changes in `bi`:**
-
-* Add big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall` and
-  `big_sepL2_forall`, `big_sepMS_forall`, `big_sepMS_impl`, and `big_sepMS_dup`.
-
 **Changes in `base_logic`:**
 
 * Add a `ghost_var` library that provides (fractional) ownership of a ghost
-- 
GitLab