From 8996e301bba28c087e3fec05533deb2e964282f2 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 8 Jan 2024 15:12:26 +0100
Subject: [PATCH] fix CHANGELOG (after rebase on top of PR #1136)

---
 CHANGELOG_UNRELEASED.md | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 66ecd9d085..878c23bb05 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -127,7 +127,7 @@
 
 - in `boolp.v`:
   + tactic `eqProp`
-  + definition `BoolProp`
+  + variant `BoolProp`
   + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
     `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
 	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
@@ -348,9 +348,6 @@
   + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}`
   + lemma `pointwise_compact_cvg`
   
--in `boolp.v`
-  - lemmas `orC` and `andC` now use `commutative`
-  
 ### Renamed
 
 ### Generalized