diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4e6bd0d72c..4667967648 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -28,6 +28,9 @@
   + instance using `isSemiAdditive.Build` for `\bar^d`
   + canonical `dEFin_snum`
 
+- in `derive.v`:
+  + lemma `cvg_at_rightE`, `cvg_at_leftE`
+
 ### Changed
 
 - in `boolp.v`:
@@ -145,6 +148,13 @@
   + canonicals `mule_monoid`, `mule_comoid` -> instance using `isComLaw.Build`
   + canonicals `maxe_monoid`, `maxe_comoid` -> instance using `isLaw.Build`
 
+- in `derive.v`
+  + in notation `'d`, `differentiable`, `is_diff`: `[filter of ...]` -> `nbhs F`
+  + canonical `mulr_linear` -> instance using `isLinear.Build`
+  + canonical `mulr_rev_linear` -> instance using `isLinear.Build`
+  + canonical `mulr_bilinear` -> lemma `mulr_is_bilinear` and instance using `bilinear_isBilinear.Build`
+  + `set (set ...)` -> `set_system ...`
+
 ### Renamed
 
 ### Generalized