fix CHANGELOG (after rebase on top of PR math-comp#1136)

Tragicus · Jan 18, 2024 · 8996e30 · 8996e30
1 parent d320b74
commit 8996e30
Showing 1 changed file with 1 addition and 4 deletions.
diff --git 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