From 0c159c48939c8f3c4064e05edf96c6a1dd00d78d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 14 Oct 2024 13:02:12 +0900 Subject: [PATCH] rm dep on topo and ereal from altreals --- theories/altreals/distr.v | 4 ++-- theories/altreals/realseq.v | 2 +- theories/altreals/realsum.v | 3 +-- 3 files changed, 4 insertions(+), 5 deletions(-) diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v index d758964f71..1402f3e310 100644 --- a/theories/altreals/distr.v +++ b/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. diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v index 7ffeb6136b..ddeb3f3a79 100644 --- a/theories/altreals/realseq.v +++ b/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. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index 900f467cea..2cb29ac962 100644 --- a/theories/altreals/realsum.v +++ b/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.