rm dep on topo and ereal from altreals

Author: affeldt-aist

theories/altreals/distr.v

@@ -6,8 +6,8 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
-Require Import xfinmap ereal reals discrete.
-Require Import topology realseq realsum.
+Require Import xfinmap constructive_ereal reals discrete.
+Require Import realseq realsum.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/altreals/realseq.v

@@ -8,7 +8,7 @@ From mathcomp Require Import all_ssreflect all_algebra.
 Require Import mathcomp.bigenough.bigenough.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.
-Require Import xfinmap ereal reals discrete topology.
+Require Import xfinmap constructive_ereal reals discrete.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/altreals/realsum.v

@@ -5,9 +5,8 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp.classical Require Import boolp.
-Require Import xfinmap ereal reals discrete realseq.
+Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
-Require Import topology.
 
 Set Implicit Arguments.
 Unset Strict Implicit.