diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f62e89d37b..399547f181 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -134,7 +134,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`,
@@ -267,16 +267,6 @@
     `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
 	 `absurd : { hyp_list(Hs) } ident(H)`
 
-
-- in `boolp.v`:
-  + tactic `eqProp`
-  + 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`,
-	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
-	 `inhabitedE`, `inhabited_witness`
-
 ### Changed
 
 - in `normedtype.v`:
@@ -318,9 +308,6 @@
 -in `boolp.v`
   - lemmas `orC` and `andC` now use `commutative`
   
--in `boolp.v`
-  - lemmas `orC` and `andC` now use `commutative`
-  
 ### Renamed
 
 - in `exp.v`: