diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 893b80843..03c90f7b0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,39 @@
 
 ### Added
 
+- file `Rstruct_topology.v`
+
+- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
+  with files
+  + `constructive_ereal.v`
+  + `reals.v`
+  + `real_interval.v`
+  + `signed.v`
+  + `itv.v`
+  + `prodnormedzmodule.v`
+  + `nsatz_realtype.v`
+  + `all_reals.v`
+
+- in file `separation_axioms.v`,
+  + new lemmas `compact_normal_local`, and `compact_normal`.
+
+- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals`
+  with files
+  + `xfinmap.v`
+  + `discrete.v`
+  + `realseq.v`
+  + `realsum.v`
+  + `distr.v`
+
+- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals`
+  with file
+  + `Rstruct.v`
+
+- package `coq-mathcomp-analysis-stdlib` depending on
+  `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files
+  + `Rstruct_topology.v`
+  + `showcase/uniform_bigO.v`
+
 - in file `separation_axioms.v`,
   + new lemmas `compact_normal_local`, and `compact_normal`.
 
@@ -31,6 +64,16 @@
      which removes the dependency on `R`.  The old formulation can be
      recovered easily with `uniform_separatorP`.
 
+- moved from `Rstruct.v` to `Rstruct_topology.v`
+  + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
+    `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
+    and `nbhs_pt_comp`
+
+- moved from `real_interval.v` to `normedtype.v`
+  + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
+    `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
+    `disj_itv_Rhull`
+
 ### Renamed
 
 ### Generalized