From d0f754954caa13c517403e2e4103d78d8c34430b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 31 Oct 2020 17:49:24 +0100
Subject: [PATCH] Update CHANGELOG for Qp changes.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9dd72474..bdfbcc73 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,7 +14,6 @@ Coq 8.8 and 8.9 are no longer supported.
   `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`.
@@ -42,8 +41,15 @@ The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
 ```
 sed -i -E '
-s/\bQp_plus/Qp_add/g
-s/\bQp_mult/Qp_mul/g
+s/\bQp_plus\b/Qp_add/g
+s/\bQp_mult\b/Qp_mul/g
+s/\bQp_mult_1_l\b/Qp_mul_1_l/g
+s/\bQp_mult_1_r\b/Qp_mul_1_r/g
+s/\bQp_plus_id_free\b/Qp_add_id_free/g
+s/\bQp_not_plus_ge\b/Qp_not_add_le_l/g
+s/\bQp_le_plus_l\b/Qp_le_add_l/g
+s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
+s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
 ' $(find theories -name "*.v")
 ```
 
-- 
GitLab