mv mathcomp_{extra,compat}

CHANGELOG_UNRELEASED.md

@@ -15,6 +15,8 @@
 
 ### Renamed
 
+- `mathcomp_extra.v` -> `mathcomp_compat.v`
+
 ### Generalized
 
 ### Deprecated

_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

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

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.

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**************************************************************************)

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                                                              *)

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                                                         *)

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                                                               *)

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                                                                  *)

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                                         *)

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_".

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 *)
+(**************************)

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.").

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                                                       *)

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.

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.

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.

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}$                                     *)

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.
 
 (* -------------------------------------------------------------------- *)

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**************************************************************************)

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.

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**************************************************************************)

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                                                          *)

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}}$)          *)

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                                            *)

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                                *)

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                         *)

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                                                  *)

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.

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.