fix

math-comp · Oct 6, 2024 · 804714f · 804714f
1 parent 258e3e6
commit 804714f
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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                                                *)