diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8924b1821..542e55de0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -168,7 +168,29 @@
 - moved from `topology.v` to `boolp.v`:
   + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
 
+- moved from `topology.v` to `separation_axioms.v`: `set_nbhs`, `set_nbhsP`,
+    `accessible_space`, `kolmogorov_space`, `hausdorff_space`,
+    `compact_closed`, `discrete_hausdorff`, `compact_cluster_set1`,
+    `compact_precompact`, `open_hausdorff`, `hausdorff_accessible`,
+    `accessible_closed_set1`, `accessible_kolmogorov`,
+    `accessible_finite_set_closed`, `subspace_hausdorff`, `order_hausdorff`,
+    `ball_hausdorff`, `Rhausdorff`, `close`, `closeEnbhs`, `closeEonbhs`,
+    `close_sym`, `cvg_close`, `close_refl`, `cvgx_close`, `cvgi_close`,
+    `cvg_toi_locally_close`, `closeE`, `close_eq`, `cvg_unique`, `cvg_eq`,
+    `cvgi_unique`, `close_cvg`, `lim_id`, `lim_near_cst`, `lim_cst`,
+    `entourage_close`, `close_trans`, `close_cvgxx`, `cvg_closeP`,
+    `ball_close`, `normal_space`, `regular_space`, `compact_regular`,
+    `uniform_regular`, `totally_disconnected`, `zero_dimensional`,
+    `discrete_zero_dimension`, `zero_dimension_totally_disconnected`,
+    `zero_dimensional_ray`, `type`, `countable_uniform_bounded`,
+    `countable_uniform`, `sup_pseudometric`, `countable_uniformityT`, `gauge`,
+    `iter_split_ent`, `gauge_ent`, `gauge_filter`, `gauge_refl`, `gauge_inv`,
+    `gauge_split`, `gauge_countable_uniformity`, `uniform_pseudometric_sup`,
+    `perfect_set`, `perfectTP`, and `perfect_set2`.
 ### Renamed
+- in file `topology.v` -> `separation_axioms.v`
+  + `totally_disconnected_cvg` -> `zero_dimensional_cvg`.
+
 
 ### Generalized
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 847b22641..bc3fe9f1c 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -118,7 +118,6 @@ Proof.
 by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->.
 Qed.
 
-
 Lemma compact_cluster_set1 (x : T) F V :
   hausdorff_space -> compact V -> nbhs x V ->
   ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
@@ -234,7 +233,6 @@ move=> npzq; exists (`]-oo, q[, `]p, +oo[)%classic; split => //=.
   by apply: npzq; exists r; rewrite rz zr.
 Qed.
 
-
 Section ball_hausdorff.
 Variables (R : numDomainType) (T : pseudoMetricType R).
 
@@ -329,8 +327,6 @@ Proof. by rewrite -closeE //; apply: cvg_close. Qed.
 Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
   {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
 Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
-
-
 End separated_topologicalType.
 
 Section separated_ptopologicalType.
@@ -370,7 +366,6 @@ Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
 Proof.
 move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
 Qed.
-
 End separated_ptopologicalType.
 
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
@@ -411,7 +406,6 @@ apply/xsectionP; apply: (entourage_split x) => //.
 by have := cxy _ (entourage_inv (entourage_split_ent entA)).
 Qed.
 
-
 Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
   F --> l <-> ([cvg F in U] /\ close (lim F) l).
 Proof.
@@ -488,8 +482,6 @@ Local Close Scope relation_scope.
 
 #[global] Hint Resolve uniform_regular : core.
 
-
-
 Section totally_disconnected.
 Implicit Types T : topologicalType.
 
@@ -574,6 +566,7 @@ exists V; split; first split.
 Qed.
 
 End totally_disconnected.
+
 (* This section proves that uniform spaces, with a countable base for their
    entourage, are metrizable. The definition of this metric is rather arcane,
    and the proof is tough. That's ok because the resulting metric is not
@@ -901,7 +894,6 @@ Qed.
 
 End countable_uniform.
 
-
 Module Exports. HB.reexport. End Exports.
 End countable_uniform.
 Export countable_uniform.Exports.
@@ -929,7 +921,6 @@ HB.instance Definition _ : PseudoMetric R S :=
 
 End sup_pseudometric.
 
-
 Module gauge.
 Section gauge.
 Local Open Scope relation_scope.
@@ -1057,4 +1048,4 @@ move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
 by move=> y [] ? [->] -> /eqP.
 Qed.
 
-End perfect_sets.
\ No newline at end of file
+End perfect_sets.