From 98cf371fa53f3a2d04d9f89db0c7c97254c60cb0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Oct 2020 12:27:55 +0100
Subject: [PATCH] move Qp changelogs entries together, and remove outdated ones

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f9783d63..9dd72474 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,15 +7,14 @@ Coq 8.8 and 8.9 are no longer supported.
 
 - Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,
   and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
-- Add `max` and `min` operations for `Qp`.
-- Add additional lemmas for `Qp`.
-- Remove the lemma `Qp_not_plus_q_ge_1` in favor of `Qp_not_plus_ge`.
 - Remove unused notations `∪**`, `∪*∪**`, `∖**`, `∖*∖**`, `⊆**`, `⊆1*`, `⊆2*`,
   `⊆1**`, `⊆2**"`, `##**`, `##1*`, `##2*`, `##1**`, `##2**` for nested
   `zip_with` and `Forall2` versions of `∪`, `∖`, and `##`.
 - Remove unused type classes `DisjointE`, `DisjointList`, `LookupE`, and
   `InsertE`.
 - Overhaul of the theory of positive rationals `Qp`:
+  + Add `max` and `min` operations for `Qp`.
+  + Add additional lemmas for `Qp`.
   + Add the orders `Qp_le` and `Qp_lt`.
   + Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent
     with the corresponding names for `nat`, `N`, and `Z`.
-- 
GitLab