diff --git a/theories/cantor.v b/theories/cantor.v
index 5408b00d7..6706dd772 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -1,11 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
-From mathcomp Require Import reals signed topology function_spaces.
-From mathcomp Require Import separation_axioms.
-From HB Require Import structures.
+Require Import reals signed topology function_spaces separation_axioms.
 
 (**md**************************************************************************)
 (* # The Cantor Space and Applications                                        *)
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index 05cc4d0c8..fcc1a68e8 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-From mathcomp Require Import reals signed topology separation_axioms.
+Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 4bd8b27fc..ca1f9c395 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -6,7 +6,6 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
-Require Import separation_axioms.
 Require Export separation_axioms.
 
 (**md**************************************************************************)
diff --git a/theories/topology.v b/theories/topology.v
index b3a18a594..cf93fafac 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
+From mathcomp Require Export filter.
 Require Import reals signed.
-Require Export filter.
 
 (**md**************************************************************************)
 (* # Basic topological notions                                                *)