more splitting or topology

_CoqProject

@@ -27,6 +27,7 @@ theories/reals.v
 theories/landau.v
 theories/Rstruct.v
 theories/topology.v
+theories/separation_axioms.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v

theories/cantor.v

@@ -4,6 +4,7 @@ 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.
 
 (**md**************************************************************************)

theories/derive.v

@@ -3,6 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 Require Import reals signed topology prodnormedzmodule normedtype landau forms.
+Require Import separation_axioms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)

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.
-Require Import reals signed topology.
+Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
@@ -1421,7 +1421,7 @@ Lemma continuous_uncurry (f : U -> V -> W) :
 Proof.
 move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //.
 move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB].
-by move=> z; exact: (@compact_regular V hsdf v B).
+by move=> z; exact: (compact_regular _ cptB).
 Qed.
 
 Lemma curry_continuous (f : (U * V)%type -> W) : continuous f -> @regular_space U ->

theories/normedtype.v

@@ -6,6 +6,8 @@ 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**************************************************************************)
 (* # Norm-related Notions                                                     *)