diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8dfb122f7..7dc6be4da 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -36,6 +36,15 @@
   + lemma `lt0_funenegM` renamed to `le0_funenegM`
     and hypothesis weakened from strict to large inequality
 
+- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v`
+
+- moved from `topology.v` to `mathcomp_extra.v`:
+  + lemma `and_prop_in`
+
+- moved from `topology.v` to `set_interval.v`:
+  + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
+  + lemmas `mem_inc_segment`, `mem_inc_segment`
+
 ### Renamed
 
 ### Generalized