From 6b0c5ce44eddd79ea12b43620a6dba77434ae9c3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 7 Aug 2026 10:39:30 +0900 Subject: [PATCH] mv mathcomp_{extra,compat} --- CHANGELOG_UNRELEASED.md | 2 ++ _CoqProject | 1 + classical/Make | 1 + classical/all_classical.v | 2 +- classical/boolp.v | 1 - classical/cardinality.v | 2 +- classical/classical_orders.v | 5 ++-- classical/classical_sets.v | 2 +- classical/filter.v | 4 ++-- classical/fsbigop.v | 3 +-- classical/functions.v | 2 +- classical/mathcomp_compat.v | 22 ++++++++++++++++++ classical/mathcomp_extra.v | 23 +++---------------- classical/set_interval.v | 3 +-- experimental_reals/distr.v | 6 ++--- experimental_reals/realseq.v | 6 ++--- experimental_reals/realsum.v | 9 ++++---- reals/constructive_ereal.v | 3 +-- reals/reals.v | 12 ++++------ theories/cantor.v | 4 ++-- theories/charge.v | 2 +- theories/convex.v | 2 +- theories/derive.v | 8 +++---- theories/ereal.v | 10 ++++---- theories/esum.v | 7 +++--- theories/exp.v | 6 ++--- theories/ftc.v | 10 ++++---- .../functional_analysis/hahn_banach_theorem.v | 7 +++--- theories/gauss_integral.v | 8 +++---- theories/hoelder.v | 6 ++--- theories/homotopy_theory/continuous_path.v | 7 +++--- theories/homotopy_theory/wedge_sigT.v | 5 ++-- theories/independence.v | 6 ++--- theories/kernel.v | 7 +++--- theories/landau.v | 9 ++++---- theories/lebesgue_integral_theory/giry.v | 5 ++-- .../lebesgue_Rintegral.v | 6 ++--- .../lebesgue_integrable.v | 6 ++--- .../lebesgue_integral_definition.v | 6 ++--- .../lebesgue_integral_differentiation.v | 6 ++--- .../lebesgue_integral_dominated_convergence.v | 6 ++--- .../lebesgue_integral_fubini.v | 6 ++--- .../lebesgue_integral_monotone_convergence.v | 6 ++--- .../lebesgue_integral_nonneg.v | 6 ++--- .../lebesgue_integral_under.v | 12 +++++----- .../measurable_fun_approximation.v | 6 ++--- .../lebesgue_integral_theory/radon_nikodym.v | 8 +++---- .../simple_functions.v | 6 ++--- theories/lebesgue_measure.v | 8 +++---- theories/measure_theory/dirac_measure.v | 9 ++++---- theories/measure_theory/measure_function.v | 5 ++-- theories/measure_theory/signed_measure.v | 8 +++---- theories/normedtype_theory/ereal_normedtype.v | 10 ++++---- theories/normedtype_theory/normed_module.v | 15 ++++++------ theories/normedtype_theory/num_normedtype.v | 2 +- theories/normedtype_theory/urysohn.v | 6 ++--- theories/numfun.v | 6 ++--- theories/pi_irrational.v | 10 ++++---- .../bernoulli_distribution.v | 3 +-- .../probability_theory/beta_distribution.v | 3 +-- .../binomial_distribution.v | 3 +-- theories/realfun.v | 8 +++---- theories/sequences.v | 6 ++--- theories/showcase/pnt.v | 8 ++++--- theories/topology_theory/function_spaces.v | 16 ++++++------- theories/topology_theory/metric_structure.v | 7 +++--- theories/topology_theory/separation_axioms.v | 15 +++++------- theories/trigo.v | 8 +++---- 68 files changed, 220 insertions(+), 234 deletions(-) create mode 100644 classical/mathcomp_compat.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9fb57d4ec6..f3bdaff1d5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,8 @@ ### Renamed +- `mathcomp_extra.v` -> `mathcomp_compat.v` + ### Generalized ### Deprecated diff --git a/_CoqProject b/_CoqProject index 21917e35d5..36f70902d7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -20,6 +20,7 @@ classical/boolp.v classical/contra.v classical/wochoice.v classical/classical_sets.v +classical/mathcomp_compat.v classical/mathcomp_extra.v classical/unstable.v classical/functions.v diff --git a/classical/Make b/classical/Make index 48b7c2d40e..229263f53e 100644 --- a/classical/Make +++ b/classical/Make @@ -14,6 +14,7 @@ boolp.v contra.v wochoice.v classical_sets.v +mathcomp_compat.v mathcomp_extra.v unstable.v functions.v diff --git a/classical/all_classical.v b/classical/all_classical.v index b70e54f614..09cbbf3e9b 100644 --- a/classical/all_classical.v +++ b/classical/all_classical.v @@ -1,7 +1,7 @@ +From mathcomp Require Export mathcomp_compat. From mathcomp Require Export boolp. From mathcomp Require Export contra. From mathcomp Require Export classical_sets. -From mathcomp Require Export mathcomp_extra. From mathcomp Require Export functions. From mathcomp Require Export cardinality. From mathcomp Require Export fsbigop. diff --git a/classical/boolp.v b/classical/boolp.v index 46c565b1d1..0234f7eeed 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -8,7 +8,6 @@ From HB Require Import structures. From mathcomp Require Import boot order. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra. From mathcomp Require internal_Eqdep_dec. (**md**************************************************************************) diff --git a/classical/cardinality.v b/classical/cardinality.v index eabfb8680a..bcc6884562 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order finmap ssralg ssrnum ssrint rat. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. (**md**************************************************************************) (* # Cardinality *) diff --git a/classical/classical_orders.v b/classical/classical_orders.v index a748ea1341..dabdb9aa1c 100644 --- a/classical/classical_orders.v +++ b/classical/classical_orders.v @@ -1,7 +1,6 @@ -From mathcomp Require Import boot order ssralg ssrnum interval. -From mathcomp Require Import mathcomp_extra boolp classical_sets. From HB Require Import structures. -From mathcomp Require Import functions set_interval. +From mathcomp Require Import boot order ssralg ssrnum interval. +From mathcomp Require Import boolp classical_sets functions set_interval. (**md**************************************************************************) (* # classical orders *) diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 763263f7d8..6f6f3158f1 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -4,7 +4,7 @@ From mathcomp Require Import boot order ssralg matrix finmap ssrnum. From mathcomp Require Import ssrint rat interval. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp wochoice. +From mathcomp Require Import boolp wochoice. (**md**************************************************************************) (* # Set Theory *) diff --git a/classical/filter.v b/classical/filter.v index 9891cd12aa..d679d446e8 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order algebra finmap. -From mathcomp Require Import boolp classical_sets functions wochoice. -From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. +From mathcomp Require Import boolp classical_sets functions wochoice + cardinality fsbigop set_interval. (**md**************************************************************************) (* # Filters *) diff --git a/classical/fsbigop.v b/classical/fsbigop.v index a68f966395..afdd16f3d1 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -2,8 +2,7 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions cardinality. +From mathcomp Require Import boolp classical_sets functions cardinality. (**md**************************************************************************) (* # Finitely-supported big operators *) diff --git a/classical/functions.v b/classical/functions.v index c0799dfedb..837bff9b03 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -3,7 +3,7 @@ From mathcomp Require Import boot order finmap ssralg ssrnum ssrint rat. From HB Require Import structures. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import boolp classical_sets. Add Search Blacklist "__canonical__". Add Search Blacklist "__functions_". Add Search Blacklist "_factory_". diff --git a/classical/mathcomp_compat.v b/classical/mathcomp_compat.v new file mode 100644 index 0000000000..6d335764f7 --- /dev/null +++ b/classical/mathcomp_compat.v @@ -0,0 +1,22 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import boot order finmap algebra. + +(**md**************************************************************************) +(* # Compatibility layer with recent MathComp versions *) +(* *) +(* This files contains lemmas and definitions recently added in mathcomp, *) +(* in order to be able to compile analysis with older versions of mathcomp. *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Local Open Scope ring_scope. + +(**************************) +(* MathComp 2.7 additions *) +(**************************) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index c8b3e846e9..06243e8463 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,22 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. -From mathcomp Require Import boot order finmap algebra. +From mathcomp Require Import mathcomp_compat. -(**md**************************************************************************) -(* # MathComp extra *) -(* *) -(* This files contains lemmas and definitions recently added in mathcomp, *) -(* in order to be able to compile analysis with older versions of mathcomp. *) -(* *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import Order.TTheory GRing.Theory Num.Theory. -Local Open Scope ring_scope. - -(**************************) -(* MathComp 2.7 additions *) -(**************************) +Attributes deprecated(since="mathcomp-analysis 1.18.0", + note="use `mathcomp_compat.v` instead."). diff --git a/classical/set_interval.v b/classical/set_interval.v index 73e94e4bcb..70d5ce566b 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -3,8 +3,7 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum interval. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions. +From mathcomp Require Import boolp classical_sets functions. (**md**************************************************************************) (* # Sets and Intervals *) diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 7283768349..bbbcf5f9e7 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -5,9 +5,9 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import boot order algebra. -From mathcomp.classical Require Import boolp classical_sets mathcomp_extra. -From mathcomp Require Import xfinmap constructive_ereal reals discrete. -From mathcomp Require Import realseq realsum. +From mathcomp Require Import boolp classical_sets. +From mathcomp Require Import constructive_ereal reals. +From mathcomp Require Import xfinmap discrete realseq realsum. Set Implicit Arguments. Unset Strict Implicit. diff --git a/experimental_reals/realseq.v b/experimental_reals/realseq.v index 1a1da4e090..99b93c39f4 100644 --- a/experimental_reals/realseq.v +++ b/experimental_reals/realseq.v @@ -6,9 +6,9 @@ (* -------------------------------------------------------------------- *) From mathcomp Require Import boot order algebra. From mathcomp Require Import bigenough. -From mathcomp.classical Require Import boolp classical_sets functions. -From mathcomp.classical Require Import mathcomp_extra. -From mathcomp Require Import xfinmap constructive_ereal reals discrete. +From mathcomp Require Import boolp classical_sets functions + constructive_ereal reals. +From mathcomp Require Import xfinmap discrete. Set Implicit Arguments. Unset Strict Implicit. diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 83ccb3421a..952fe9f99f 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -4,14 +4,13 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import boot order algebra. +From mathcomp Require Import boot order algebra interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import boolp fsbigop classical_sets functions. -From mathcomp Require Import cardinality. -From mathcomp Require Import constructive_ereal reals. +From mathcomp Require Import boolp fsbigop classical_sets functions cardinality. +From mathcomp Require Import reals. +From mathcomp Require Import ereal esum numfun. From mathcomp Require Import xfinmap discrete realseq. -From mathcomp Require Import esum ereal numfun. Set Implicit Arguments. Unset Strict Implicit. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index eb15247e53..e838c7ebdc 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -10,8 +10,7 @@ incorporate it into mathcomp proper where it could then be used for bounds of intervals*) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. -From mathcomp Require Import mathcomp_extra interval_inference. +From mathcomp Require Import boot order algebra finmap interval_inference. (**md**************************************************************************) (* # Extended real numbers $\overline{R}$ *) diff --git a/reals/reals.v b/reals/reals.v index 8c724dd0b6..ef3fd591b4 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -4,6 +4,11 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) +From HB Require Import structures. +From mathcomp Require Import boot order algebra. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import boolp classical_sets contra set_interval. (**md**************************************************************************) (* # An axiomatization of real numbers $\mathbb{R}$ *) @@ -43,13 +48,6 @@ (* *) (******************************************************************************) -From HB Require Import structures. -From mathcomp Require Import boot order algebra. -#[warning="-warn-library-file-internal-analysis"] -From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets contra - set_interval. - Declare Scope real_scope. (* -------------------------------------------------------------------- *) diff --git a/theories/cantor.v b/theories/cantor.v index e2155843cd..8282e8e09a 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -1,8 +1,8 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrint ssrnum interval. From mathcomp Require Import rat finmap. -From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. +From mathcomp Require Import unstable boolp classical_sets. From mathcomp Require Import functions cardinality reals topology. (**md**************************************************************************) diff --git a/theories/charge.v b/theories/charge.v index 5dfcd3b646..be5c930d90 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -4,7 +4,7 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap fingroup perm rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. +From mathcomp Require Import boolp classical_sets cardinality. From mathcomp Require Import functions fsbigop set_interval reals ereal. From mathcomp Require Import topology numfun normedtype derive sequences esum. From mathcomp Require Import measure realfun measurable_realfun. diff --git a/theories/convex.v b/theories/convex.v index 98ede3af01..89dccb9c51 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -4,7 +4,7 @@ From mathcomp Require Import boot order finmap ssralg ssrint ssrnum interval. From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. +From mathcomp Require Import boolp classical_sets set_interval. From mathcomp Require Import reals topology. (**md**************************************************************************) diff --git a/theories/derive.v b/theories/derive.v index 33b99954aa..3fb22e1456 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,12 +1,12 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order ssralg ssrnum matrix interval. +From mathcomp Require Import boot order ssralg ssrnum matrix interval + interval_inference. From mathcomp Require Import poly sesquilinear. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp contra classical_sets. -From mathcomp Require Import functions reals interval_inference topology. -From mathcomp Require Import prodnormedzmodule tvs normedtype landau. +From mathcomp Require Import boolp contra classical_sets functions reals. +From mathcomp Require Import topology prodnormedzmodule tvs normedtype landau. (**md**************************************************************************) (* # Differentiation *) diff --git a/theories/ereal.v b/theories/ereal.v index 8becb5ed50..4243e101e8 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -5,12 +5,14 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. +From mathcomp Require Import boot order algebra interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import fsbigop cardinality set_interval reals. -From mathcomp Require Export interval_inference topology constructive_ereal. +From mathcomp Require Import boolp classical_sets functions fsbigop cardinality + set_interval. +From mathcomp Require Import reals. +From mathcomp Require Export constructive_ereal. +From mathcomp Require Import topology. (**md**************************************************************************) (* # Extended real numbers, classical part ($\overline{\mathbb{R}}$) *) diff --git a/theories/esum.v b/theories/esum.v index dcedd52ddf..b6b6b231b8 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import boot order ssralg ssrnum finmap. +From mathcomp Require Import boot order ssralg ssrnum interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal interval_inference. -From mathcomp Require Import topology sequences normedtype numfun. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals topology ereal sequences normedtype numfun. (**md**************************************************************************) (* # Summation over classical sets *) diff --git a/theories/exp.v b/theories/exp.v index 690794d02c..8ecd84bd5b 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -3,9 +3,9 @@ From mathcomp Require Import boot order ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import boolp classical_sets functions mathcomp_extra. -From mathcomp Require Import reals topology ereal tvs normedtype landau. -From mathcomp Require Import sequences derive realfun convex. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import reals convex ereal topology tvs normedtype landau. +From mathcomp Require Import sequences derive realfun. (**md**************************************************************************) (* # Theory of exponential/logarithm functions *) diff --git a/theories/ftc.v b/theories/ftc.v index ec0f87e52c..25a17f2d0e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -4,12 +4,10 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. -From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. -From mathcomp Require Import interval_inference real_interval lebesgue_integral. -From mathcomp Require Import derive. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs normedtype + derive sequences esum measure lebesgue_measure numfun realfun + measurable_realfun lebesgue_integral. (**md**************************************************************************) (* # Fundamental Theorem of Calculus and Consequences *) diff --git a/theories/functional_analysis/hahn_banach_theorem.v b/theories/functional_analysis/hahn_banach_theorem.v index 35d2c25d50..c29a495541 100644 --- a/theories/functional_analysis/hahn_banach_theorem.v +++ b/theories/functional_analysis/hahn_banach_theorem.v @@ -1,10 +1,9 @@ From HB Require Import structures. -From mathcomp Require Import boot order algebra. -From mathcomp Require Import interval_inference. +From mathcomp Require Import boot order algebra interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp contra classical_sets filter. -From mathcomp Require Import topology convex reals normedtype. +From mathcomp Require Import boolp contra classical_sets filter. +From mathcomp Require Import reals convex topology normedtype. (**md**************************************************************************) (* # The Hahn-Banach theorem *) diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index acaf3b7bec..cac9ef90cb 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -1,9 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import boot order ssralg ssrnum ssrint interval_inference + interval finmap. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals ereal. From mathcomp Require Import topology tvs normedtype sequences real_interval. From mathcomp Require Import esum measure measurable_realfun numfun realfun. From mathcomp Require Import exp trigo lebesgue_measure lebesgue_integral. diff --git a/theories/hoelder.v b/theories/hoelder.v index 06d7cb6675..27aa991863 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality convex fsbigop reals ereal topology. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import convex reals real_interval ereal topology. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import ess_sup_inf measurable_realfun lebesgue_measure. From mathcomp Require Import lebesgue_integral numfun exp. diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index b21677eafc..6ed100fde3 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -1,9 +1,8 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order generic_quotient algebra. -From mathcomp Require Import finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT. +From mathcomp Require Import boot order generic_quotient algebra finmap. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals topology wedge_sigT. (**md**************************************************************************) (* # Paths *) diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 1c4ca3c754..21cf3099b8 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra generic_quotient. -From mathcomp Require Import finmap. +From mathcomp Require Import boot order algebra generic_quotient finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals topology. (**md**************************************************************************) diff --git a/theories/independence.v b/theories/independence.v index 7778965f5c..41fda5c04d 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -2,10 +2,10 @@ From HB Require Import structures. From mathcomp Require Import boot order interval_inference. From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals. +From mathcomp Require Import ereal topology normedtype sequences. From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. -From mathcomp Require Import reals ereal topology normedtype sequences. From mathcomp Require Import esum measure exp numfun lebesgue_measure. From mathcomp Require Import measurable_realfun lebesgue_integral kernel. From mathcomp Require Import hoelder probability. diff --git a/theories/kernel.v b/theories/kernel.v index ac2229d7df..cbae018431 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -2,10 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal topology. -From mathcomp Require Import normedtype sequences esum measure. -From mathcomp Require Import measurable_realfun numfun lebesgue_measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals topology ereal normedtype sequences esum. +From mathcomp Require Import measure measurable_realfun numfun lebesgue_measure. From mathcomp Require Import lebesgue_integral. (**md**************************************************************************) diff --git a/theories/landau.v b/theories/landau.v index e386ebdb14..d111ee3039 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -1,9 +1,8 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order ssralg ssrnum. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import ereal reals interval_inference topology normedtype. -From mathcomp Require Import prodnormedzmodule. +From mathcomp Require Import boot order ssralg interval_inference ssrnum. +From mathcomp Require Import boolp classical_sets functions reals. +From mathcomp Require Import ereal topology normedtype prodnormedzmodule. (**md**************************************************************************) (* # Bachmann-Landau notations: $f=o(e)$, $f=O(e)$ *) diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index 21b399cb4c..95f51f589c 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -1,6 +1,7 @@ From HB Require Import structures. -From mathcomp Require Import boot order algebra boolp classical_sets. -From mathcomp Require Import fsbigop functions reals topology separation_axioms. +From mathcomp Require Import boot order algebra interval_inference. +From mathcomp Require Import boolp classical_sets fsbigop functions. +From mathcomp Require Import reals topology separation_axioms. From mathcomp Require Import ereal sequences numfun measure measurable_realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral. diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index c6a3bd1c5e..6327d6b5e1 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -2,9 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. From mathcomp Require Import simple_functions measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 706a0a57b4..a4b4a5f741 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 31c868b184..faca643b80 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 3178a40fbd..725a47558a 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -2,9 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 99200b049e..0762caa9e5 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -2,9 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index a5f62220c8..66bac6b7af 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -2,9 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index d3d54b65d0..236aafdd67 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 9c8a37166b..36b5720881 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v index 9d5edf6708..286e4d8d25 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v @@ -2,14 +2,14 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval derive esum. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval ereal topology tvs. +From mathcomp Require Import normedtype sequences derive esum. From mathcomp Require Import measure lebesgue_measure numfun realfun. From mathcomp Require Import measurable_realfun simple_functions. -From mathcomp Require Import lebesgue_integral_definition lebesgue_integral_nonneg. -From mathcomp Require Import lebesgue_integrable lebesgue_Rintegral. -From mathcomp Require Import lebesgue_integral_dominated_convergence. +From mathcomp Require Import lebesgue_integral_definition + lebesgue_integral_nonneg lebesgue_integrable lebesgue_Rintegral + lebesgue_integral_dominated_convergence. (**md**************************************************************************) (* # Continuity and differentiation under the integral sign *) diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 76d6665226..5fd4bb87e3 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun exp. From mathcomp Require Import measurable_realfun simple_functions. diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v index 6197cdb652..161f6cffd1 100644 --- a/theories/lebesgue_integral_theory/radon_nikodym.v +++ b/theories/lebesgue_integral_theory/radon_nikodym.v @@ -4,10 +4,10 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap fingroup perm rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. -From mathcomp Require Import functions fsbigop set_interval reals ereal. -From mathcomp Require Import topology numfun normedtype derive sequences esum. -From mathcomp Require Import measure realfun measurable_realfun. +From mathcomp Require Import boolp classical_sets cardinality functions fsbigop + set_interval reals. +From mathcomp Require Import topology ereal numfun normedtype derive sequences. +From mathcomp Require Import esum measure realfun measurable_realfun. From mathcomp Require Import lebesgue_measure. From mathcomp Require Import lebesgue_integral_definition lebesgue_integrable lebesgue_integral_nonneg lebesgue_Rintegral diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 04e9cc138a..4f95cc02ac 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -2,9 +2,9 @@ From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference archimedean finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal tvs. +From mathcomp Require Import normedtype sequences esum measure. From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. (**md**************************************************************************) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e20685b53d..0e0f99382f 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -4,10 +4,10 @@ From mathcomp Require Import boot order finmap ssralg ssrnum ssrint. From mathcomp Require Import interval interval_inference archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals ereal topology numfun. -From mathcomp Require Import tvs normedtype sequences esum measure. -From mathcomp Require Import real_interval realfun exp measurable_realfun. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop + reals real_interval. +From mathcomp Require Import topology ereal numfun tvs normedtype sequences + esum measure realfun exp measurable_realfun. From mathcomp Require Export lebesgue_stieltjes_measure. (**md**************************************************************************) diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v index dbda7cf63b..4509245a8f 100644 --- a/theories/measure_theory/dirac_measure.v +++ b/theories/measure_theory/dirac_measure.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop reals. -From mathcomp Require Import interval_inference ereal topology normedtype. -From mathcomp Require Import sequences esum numfun. +From mathcomp Require Import boot order algebra interval_inference finmap. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop + reals. +From mathcomp Require Import topology ereal normedtype sequences esum numfun. From mathcomp Require Import measurable_structure measure_function. (**md**************************************************************************) diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 57526df8eb..b84ba58366 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1,11 +1,10 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. +From mathcomp Require Import boot order algebra interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals interval_inference ereal topology normedtype. -From mathcomp Require Import sequences esum. +From mathcomp Require Import reals ereal topology normedtype sequences esum. From mathcomp Require Import measurable_structure measurable_function. (**md**************************************************************************) diff --git a/theories/measure_theory/signed_measure.v b/theories/measure_theory/signed_measure.v index 7590e36026..5b14db1b26 100644 --- a/theories/measure_theory/signed_measure.v +++ b/theories/measure_theory/signed_measure.v @@ -4,10 +4,10 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap fingroup perm rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. -From mathcomp Require Import functions fsbigop set_interval reals ereal. -From mathcomp Require Import topology numfun normedtype derive sequences esum. -From mathcomp Require Import measurable_structure measurable_function. +From mathcomp Require Import boolp classical_sets cardinality functions fsbigop. +From mathcomp Require Import set_interval reals. +From mathcomp Require Import topology ereal numfun normedtype derive sequences. +From mathcomp Require Import esum measurable_structure measurable_function. From mathcomp Require Import measure_function measure_negligible. (**md**************************************************************************) diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index d3c3d6e75f..1d88f050f5 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/theories/normedtype_theory/ereal_normedtype.v @@ -1,9 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order ssralg ssrnum interval. -From mathcomp Require Import interval_inference. -From mathcomp Require Import boolp classical_sets ereal reals topology. -From mathcomp Require Import real_interval num_normedtype. +From mathcomp Require Import boot order ssralg ssrnum interval + interval_inference. +From mathcomp Require Import boolp classical_sets ereal reals real_interval. +From mathcomp Require Import topology ereal num_normedtype. (**md**************************************************************************) (* # Preliminaries for norm-related notions *) @@ -41,7 +41,7 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. Section limf_esup_einf. -Variables (T : choiceType) (X : filteredType T) (R : realFieldType). +Context {T : choiceType} {X : filteredType T} {R : realFieldType}. Implicit Types (f : X -> \bar R) (F : set_system X). Local Open Scope ereal_scope. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 706671a82a..4d9d64b92a 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1,13 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order finmap ssralg ssrnum ssrint. -From mathcomp Require Import archimedean rat interval zmodp vector. +From mathcomp Require Import boot order finmap ssralg ssrnum ssrint + interval_inference archimedean rat interval zmodp vector. #[warning="-warn-library-file-internal-analysis"] -From mathcomp Require Import mathcomp_extra unstable. -From mathcomp Require Import boolp classical_sets filter functions cardinality. -From mathcomp Require Import set_interval ereal reals topology real_interval. -From mathcomp Require Import convex prodnormedzmodule tvs num_normedtype. -From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. +From mathcomp Require Import unstable. +From mathcomp Require Import boolp classical_sets filter functions cardinality + set_interval. +From mathcomp Require Import reals real_interval ereal topology convex + prodnormedzmodule tvs num_normedtype ereal_normedtype + pseudometric_normed_Zmodule. (**md**************************************************************************) (* # Normed modules *) diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 5ae913e592..f6616b6f6a 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -3,7 +3,7 @@ From mathcomp Require Import boot order finmap ssralg ssrnum ssrint. From mathcomp Require Import interval interval_inference archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality set_interval reals real_interval. From mathcomp Require Import topology prodnormedzmodule. diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index 37a937a873..bc0e9a656d 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -5,9 +5,9 @@ From mathcomp Require Import interval interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval ereal reals topology tvs. -From mathcomp Require Import num_normedtype pseudometric_normed_Zmodule. -From mathcomp Require Import normed_module. +From mathcomp Require Import set_interval reals. +From mathcomp Require Import topology ereal tvs num_normedtype. +From mathcomp Require Import pseudometric_normed_Zmodule normed_module. (**md**************************************************************************) (* # Urysohn's lemma *) diff --git a/theories/numfun.v b/theories/numfun.v index e8b8a67382..c29703ca18 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. -From mathcomp Require Import functions cardinality set_interval reals ereal. -From mathcomp Require Import topology normedtype sequences. +From mathcomp Require Import boolp classical_sets fsbigop functions cardinality + set_interval reals. +From mathcomp Require Import topology ereal normedtype sequences. (**md**************************************************************************) (* # Numerical functions *) diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 81cffb88da..e563fb78c1 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -1,10 +1,8 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import boot order algebra. -From mathcomp Require Import interval_inference. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop. -From mathcomp Require Import reals ereal topology normedtype sequences. -From mathcomp Require Import real_interval esum measure measurable_realfun. +From mathcomp Require Import boot order algebra interval_inference. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals real_interval topology ereal normedtype. +From mathcomp Require Import sequences esum measure measurable_realfun. From mathcomp Require Import numfun realfun lebesgue_measure lebesgue_integral. From mathcomp Require Import derive ftc trigo. diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index 245a5777ec..267d1739a7 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -4,9 +4,8 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals ereal topology normedtype sequences esum. +From mathcomp Require Import reals topology ereal normedtype sequences esum. From mathcomp Require Import measure numfun measurable_realfun lebesgue_measure. From mathcomp Require Import lebesgue_integral kernel. diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index 1573d70805..f5dbeb5643 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -4,9 +4,8 @@ From mathcomp Require Import boot order ssralg poly ssrnum ssrint. From mathcomp Require Import archimedean finmap interval interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals ereal topology normedtype sequences derive. +From mathcomp Require Import reals topology ereal normedtype sequences derive. From mathcomp Require Import measure exp numfun realfun measurable_realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral ftc. From mathcomp Require Import uniform_distribution bernoulli_distribution. diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v index 650045867e..3d7bf37b0c 100644 --- a/theories/probability_theory/binomial_distribution.v +++ b/theories/probability_theory/binomial_distribution.v @@ -4,9 +4,8 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals ereal topology normedtype sequences esum. +From mathcomp Require Import reals topology ereal normedtype sequences esum. From mathcomp Require Import measure measurable_realfun lebesgue_measure. From mathcomp Require Import lebesgue_integral bernoulli_distribution. diff --git a/theories/realfun.v b/theories/realfun.v index 1ee878c7f0..e7bf5f3a72 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -4,10 +4,10 @@ From mathcomp Require Import boot order finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean interval interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality contra reals convex ereal. -From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. -From mathcomp Require Import sequences real_interval numfun. +From mathcomp Require Import boolp classical_sets functions cardinality contra. +From mathcomp Require Import reals convex. +From mathcomp Require Import topology ereal prodnormedzmodule tvs normedtype. +From mathcomp Require Import derive sequences real_interval numfun. (**md**************************************************************************) (* # Real-valued functions over reals *) diff --git a/theories/sequences.v b/theories/sequences.v index fff6e799e9..a60149df00 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -4,9 +4,9 @@ From mathcomp Require Import boot order ssralg ssrnum ssrint. From mathcomp Require Import interval interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp contra classical_sets. -From mathcomp Require Import functions cardinality set_interval reals. -From mathcomp Require Import ereal topology tvs normedtype landau. +From mathcomp Require Import boolp contra classical_sets functions cardinality + set_interval reals. +From mathcomp Require Import topology ereal tvs normedtype landau. (**md**************************************************************************) (* # Definitions and lemmas about sequences *) diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v index 23c7e3b842..d5ab3911cb 100644 --- a/theories/showcase/pnt.v +++ b/theories/showcase/pnt.v @@ -1,9 +1,9 @@ -From mathcomp Require Import boot order ssralg ssrnum ssrint interval. +From mathcomp Require Import boot order ssralg ssrnum ssrint interval + interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import classical_sets boolp topology. -From mathcomp Require Import ereal sequences reals. -Import Order.POrderTheory GRing.Theory Num.Theory. +From mathcomp Require Import reals ereal sequences. (**md**************************************************************************) (* # The Prime Number Theorem *) @@ -27,6 +27,8 @@ Local Open Scope classical_set_scope. Local Open Scope set_scope. Local Open Scope nat_scope. +Import Order.POrderTheory GRing.Theory Num.Theory. + Section prime_seq. Let next_prime_subproof n : {i : 'I_(n`! - n).+1 | prime (n.+1 + i)}. diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v index 9d01bf5b3b..70267952ec 100644 --- a/theories/topology_theory/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -1,16 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. -From mathcomp Require Import generic_quotient. +From mathcomp Require Import boot order algebra interval_inference. +From mathcomp Require Import generic_quotient finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals interval_inference. -From mathcomp Require Import topology_structure uniform_structure. -From mathcomp Require Import supremum_topology initial_topology. -From mathcomp Require Import pseudometric_structure separation_axioms. -From mathcomp Require Import compact connected subspace_topology. -From mathcomp Require Import product_topology. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals. +From mathcomp Require Import topology_structure uniform_structure + supremum_topology initial_topology pseudometric_structure separation_axioms + compact connected subspace_topology product_topology. (**md**************************************************************************) (* # The topology of functions spaces *) diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index ee6eda7fe9..a64e3e9eb3 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -5,10 +5,9 @@ From mathcomp Require Import interval_inference rat interval zmodp vector. From mathcomp Require Import fieldext falgebra archimedean finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import contra reals topology_structure. -From mathcomp Require Import uniform_structure pseudometric_structure. -From mathcomp Require Import num_topology product_topology separation_axioms. +From mathcomp Require Import boolp classical_sets contra reals. +From mathcomp Require Import topology_structure uniform_structure + pseudometric_structure num_topology product_topology separation_axioms. (**md**************************************************************************) (* # Metric spaces *) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 695e9bd33f..60ff99a030 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1,14 +1,12 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order algebra finmap. +From mathcomp Require Import boot order algebra interval_inference finmap. From mathcomp Require Import boolp classical_sets functions wochoice. -From mathcomp Require Import cardinality fsbigop. -From mathcomp Require Import set_interval filter reals interval_inference. -From mathcomp Require Import topology_structure compact subspace_topology. -From mathcomp Require Import discrete_topology order_topology. -From mathcomp Require Import pseudometric_structure num_topology. -From mathcomp Require Import one_point_compactification uniform_structure. -From mathcomp Require Import connected supremum_topology sigT_topology. +From mathcomp Require Import cardinality fsbigop set_interval filter reals. +From mathcomp Require Import topology_structure compact subspace_topology + discrete_topology order_topology pseudometric_structure num_topology + one_point_compactification uniform_structure connected supremum_topology + sigT_topology. (**md**************************************************************************) (* # Separation Axioms *) @@ -59,7 +57,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. -From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. diff --git a/theories/trigo.v b/theories/trigo.v index b0e9f949ec..383cdc4068 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1,11 +1,11 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import boot order ssralg ssrint ssrnum matrix. -From mathcomp Require Import interval rat. +From mathcomp Require Import boot order ssralg ssrint ssrnum matrix + interval_inference interval rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import reals ereal interval_inference topology normedtype. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import reals topology ereal normedtype. From mathcomp Require Import landau sequences derive realfun exp realfun. From mathcomp Require Import measure lebesgue_measure lebesgue_integral ftc.