From 641fa463e3d872fbdcaaba5f3197c8e2842e95b8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Feb 2026 14:57:40 +0100 Subject: [PATCH 1/2] Add compat file for all_ssreflect rocqPackages.mathcomp already dropped all_ssreflect and we cannot use all_boot/all_order until we require MC >= 2.5, so resorting to this compat file meanwhile. --- _CoqProject | 1 + analysis_stdlib/Rstruct_topology.v | 2 +- classical/Make | 1 + classical/all_ssreflect_compat.v | 21 +++++++++++++++++++ classical/boolp.v | 2 +- classical/cardinality.v | 2 +- classical/classical_orders.v | 2 +- classical/classical_sets.v | 2 +- classical/filter.v | 2 +- classical/fsbigop.v | 2 +- classical/functions.v | 2 +- classical/mathcomp_extra.v | 2 +- classical/set_interval.v | 2 +- classical/unstable.v | 2 +- experimental_reals/dedekind.v | 2 +- experimental_reals/discrete.v | 2 +- experimental_reals/distr.v | 2 +- experimental_reals/realseq.v | 2 +- experimental_reals/realsum.v | 2 +- experimental_reals/xfinmap.v | 2 +- reals/constructive_ereal.v | 2 +- reals/prodnormedzmodule.v | 2 +- reals/real_interval.v | 2 +- reals/reals.v | 2 +- reals_stdlib/Rstruct.v | 2 +- reals_stdlib/nsatz_realtype.v | 2 +- theories/borel_hierarchy.v | 2 +- theories/cantor.v | 2 +- theories/charge.v | 2 +- theories/convex.v | 2 +- theories/derive.v | 2 +- theories/ereal.v | 2 +- theories/ess_sup_inf.v | 2 +- theories/esum.v | 2 +- theories/exp.v | 2 +- theories/ftc.v | 2 +- theories/function_spaces.v | 2 +- theories/gauss_integral.v | 2 +- theories/hoelder.v | 2 +- theories/homotopy_theory/continuous_path.v | 2 +- theories/homotopy_theory/wedge_sigT.v | 2 +- theories/kernel.v | 2 +- theories/landau.v | 2 +- theories/lebesgue_integral_theory/giry.v | 2 +- .../lebesgue_Rintegral.v | 2 +- .../lebesgue_integrable.v | 2 +- .../lebesgue_integral_definition.v | 2 +- .../lebesgue_integral_differentiation.v | 2 +- .../lebesgue_integral_dominated_convergence.v | 2 +- .../lebesgue_integral_fubini.v | 2 +- .../lebesgue_integral_monotone_convergence.v | 2 +- .../lebesgue_integral_nonneg.v | 2 +- .../lebesgue_integral_under.v | 2 +- .../measurable_fun_approximation.v | 2 +- .../simple_functions.v | 2 +- theories/lebesgue_measure.v | 2 +- theories/lebesgue_stieltjes_measure.v | 2 +- theories/measurable_realfun.v | 2 +- theories/measure_theory/counting_measure.v | 2 +- theories/measure_theory/dirac_measure.v | 2 +- theories/measure_theory/measurable_function.v | 2 +- .../measure_theory/measurable_structure.v | 2 +- theories/measure_theory/measure_extension.v | 2 +- theories/measure_theory/measure_function.v | 2 +- theories/measure_theory/measure_negligible.v | 2 +- theories/measure_theory/probability_measure.v | 2 +- .../complete_normed_module.v | 2 +- theories/normedtype_theory/ereal_normedtype.v | 2 +- .../normedtype_theory/matrix_normedtype.v | 2 +- theories/normedtype_theory/normed_module.v | 2 +- theories/normedtype_theory/num_normedtype.v | 2 +- .../pseudometric_normed_Zmodule.v | 2 +- theories/normedtype_theory/urysohn.v | 2 +- theories/normedtype_theory/vitali_lemma.v | 2 +- theories/numfun.v | 2 +- theories/pi_irrational.v | 2 +- .../bernoulli_distribution.v | 2 +- .../probability_theory/beta_distribution.v | 2 +- .../binomial_distribution.v | 2 +- .../exponential_distribution.v | 2 +- .../probability_theory/normal_distribution.v | 2 +- .../probability_theory/poisson_distribution.v | 2 +- theories/probability_theory/random_variable.v | 2 +- .../probability_theory/uniform_distribution.v | 2 +- theories/realfun.v | 2 +- theories/sequences.v | 2 +- theories/showcase/pnt.v | 2 +- theories/showcase/summability.v | 2 +- theories/topology_theory/bool_topology.v | 2 +- theories/topology_theory/compact.v | 2 +- theories/topology_theory/connected.v | 2 +- theories/topology_theory/discrete_topology.v | 2 +- theories/topology_theory/initial_topology.v | 2 +- theories/topology_theory/matrix_topology.v | 2 +- theories/topology_theory/metric_structure.v | 2 +- theories/topology_theory/nat_topology.v | 2 +- theories/topology_theory/num_topology.v | 2 +- .../one_point_compactification.v | 2 +- theories/topology_theory/order_topology.v | 2 +- theories/topology_theory/product_topology.v | 2 +- .../topology_theory/pseudometric_structure.v | 2 +- theories/topology_theory/quotient_topology.v | 2 +- theories/topology_theory/separation_axioms.v | 2 +- theories/topology_theory/sigT_topology.v | 2 +- theories/topology_theory/subspace_topology.v | 2 +- theories/topology_theory/subtype_topology.v | 2 +- theories/topology_theory/supremum_topology.v | 2 +- theories/topology_theory/topology_structure.v | 2 +- theories/topology_theory/uniform_structure.v | 2 +- theories/topology_theory/weak_topology.v | 2 +- theories/trigo.v | 2 +- theories/tvs.v | 2 +- 112 files changed, 132 insertions(+), 109 deletions(-) create mode 100644 classical/all_ssreflect_compat.v diff --git a/_CoqProject b/_CoqProject index de1083c007..fdbf17db9c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -14,6 +14,7 @@ classical/all_classical.v classical/internal_Eqdep_dec.v +classical/all_ssreflect_compat.v classical/boolp.v classical/contra.v classical/wochoice.v diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 8506459984..330d17b638 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -8,7 +8,7 @@ Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. Require Import Rtrigo1 Reals. From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum archimedean. From mathcomp Require Import boolp classical_sets reals interval_inference. From mathcomp Require Export Rstruct. From mathcomp Require Import topology. diff --git a/classical/Make b/classical/Make index ad0313df56..671e16f7b4 100644 --- a/classical/Make +++ b/classical/Make @@ -8,6 +8,7 @@ -arg -w -arg -projection-no-head-constant internal_Eqdep_dec.v +all_ssreflect_compat.v boolp.v contra.v wochoice.v diff --git a/classical/all_ssreflect_compat.v b/classical/all_ssreflect_compat.v new file mode 100644 index 0000000000..990a7030dd --- /dev/null +++ b/classical/all_ssreflect_compat.v @@ -0,0 +1,21 @@ +(* Remove this file and use all_boot/all_order when requiring MC >= 2.5.0 *) +From mathcomp Require Export ssreflect. +From mathcomp Require Export ssrbool. +From mathcomp Require Export ssrfun. +From mathcomp Require Export eqtype. +From mathcomp Require Export ssrnat. +From mathcomp Require Export seq. +From mathcomp Require Export choice. +From mathcomp Require Export path. +From mathcomp Require Export div. +From mathcomp Require Export fintype. +From mathcomp Require Export fingraph. +From mathcomp Require Export tuple. +From mathcomp Require Export finfun. +From mathcomp Require Export bigop. +From mathcomp Require Export prime. +From mathcomp Require Export finset. +From mathcomp Require Export binomial. +From mathcomp Require Export generic_quotient. +From mathcomp Require Export ssrAC. +From mathcomp Require Export order. diff --git a/classical/boolp.v b/classical/boolp.v index 99fef686dc..ac856a3d23 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -5,7 +5,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect. +From mathcomp Require Import all_ssreflect_compat. From mathcomp Require Import mathcomp_extra. From mathcomp Require internal_Eqdep_dec. diff --git a/classical/cardinality.v b/classical/cardinality.v index a4f2dae11c..48f5ed643a 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint rat. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. (**md**************************************************************************) diff --git a/classical/classical_orders.v b/classical/classical_orders.v index 9d2eefccdb..4da4cba4c9 100644 --- a/classical/classical_orders.v +++ b/classical/classical_orders.v @@ -1,4 +1,4 @@ -From mathcomp Require Import all_ssreflect ssralg ssrnum interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum interval. From mathcomp Require Import mathcomp_extra boolp classical_sets. From HB Require Import structures. From mathcomp Require Import functions set_interval. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 664dbf4ee8..167c0368f8 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg matrix finmap ssrnum. +From mathcomp Require Import all_ssreflect_compat ssralg matrix finmap ssrnum. From mathcomp Require Import ssrint rat interval. From mathcomp Require Import mathcomp_extra boolp wochoice. diff --git a/classical/filter.v b/classical/filter.v index 0d2f6d45f1..62cbb550bb 100644 --- a/classical/filter.v +++ b/classical/filter.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. From mathcomp Require Import boolp classical_sets functions wochoice. From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval. diff --git a/classical/fsbigop.v b/classical/fsbigop.v index e0fc85da63..52ccca2ec8 100644 --- a/classical/fsbigop.v +++ b/classical/fsbigop.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat 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. diff --git a/classical/functions.v b/classical/functions.v index 21961e61b9..a8a65817de 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint rat. From HB Require Import structures. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f9dd338c0e..32fa8b517b 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. (**md**************************************************************************) (* # MathComp extra *) diff --git a/classical/set_interval.v b/classical/set_interval.v index e0d26aaa63..e19d73cf45 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum interval. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets. diff --git a/classical/unstable.v b/classical/unstable.v index da4e0b8087..fe7953eeb4 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean interval. (**md**************************************************************************) diff --git a/experimental_reals/dedekind.v b/experimental_reals/dedekind.v index cfc4cb8251..4bc22fd540 100644 --- a/experimental_reals/dedekind.v +++ b/experimental_reals/dedekind.v @@ -7,7 +7,7 @@ (* SSReflect hierarchy (see reals.v) *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From Coq Require Import Setoid. (* -------------------------------------------------------------------- *) diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b8..79bc14c24e 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -6,7 +6,7 @@ (* -------------------------------------------------------------------- *) From Corelib Require Setoid. From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp.classical Require Import boolp. From mathcomp Require Import xfinmap reals. diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v index 37fe02f40a..3d40a0acbf 100644 --- a/experimental_reals/distr.v +++ b/experimental_reals/distr.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_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. diff --git a/experimental_reals/realseq.v b/experimental_reals/realseq.v index 493553e90e..fb76cfb59c 100644 --- a/experimental_reals/realseq.v +++ b/experimental_reals/realseq.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import bigenough. From mathcomp.classical Require Import boolp classical_sets functions. From mathcomp.classical Require Import mathcomp_extra. diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v index 93067f4cdf..4418622a18 100644 --- a/experimental_reals/realsum.v +++ b/experimental_reals/realsum.v @@ -3,7 +3,7 @@ (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp.classical Require Import boolp. From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq. From mathcomp.classical Require Import classical_sets functions. diff --git a/experimental_reals/xfinmap.v b/experimental_reals/xfinmap.v index 85eae7ff5a..63f93afe32 100644 --- a/experimental_reals/xfinmap.v +++ b/experimental_reals/xfinmap.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Export finmap. Set Implicit Arguments. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 14eba026af..996ef3cd23 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -10,7 +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 all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. From mathcomp Require Import mathcomp_extra interval_inference. (**md**************************************************************************) diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v index fcc5c58acb..855205985a 100644 --- a/reals/prodnormedzmodule.v +++ b/reals/prodnormedzmodule.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2020 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum. +From mathcomp Require Import all_ssreflect_compat fingroup ssralg poly ssrnum. From mathcomp Require Import all_classical. From mathcomp Require Import interval_inference. diff --git a/reals/real_interval.v b/reals/real_interval.v index 4beab5562b..97cbcf97ab 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Export set_interval. diff --git a/reals/reals.v b/reals/reals.v index 1a6685839d..23d8a302fe 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -44,7 +44,7 @@ (******************************************************************************) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index eff6041d52..13c675a0d8 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -3,7 +3,7 @@ From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf. From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. From Coq Require Import Rtrigo1 Reals. From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg poly ssrnum archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg poly ssrnum archimedean. (**md**************************************************************************) diff --git a/reals_stdlib/nsatz_realtype.v b/reals_stdlib/nsatz_realtype.v index 13ac17f8ab..dfff679cf4 100644 --- a/reals_stdlib/nsatz_realtype.v +++ b/reals_stdlib/nsatz_realtype.v @@ -1,5 +1,5 @@ From Coq Require Import Nsatz. -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum. From mathcomp Require Import boolp reals constructive_ereal. (**md**************************************************************************) diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 4095425bcc..cb6a8ea5a7 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -1,4 +1,4 @@ -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals topology normedtype sequences. From mathcomp Require Import measure lebesgue_measure. diff --git a/theories/cantor.v b/theories/cantor.v index a8ff6eae91..8803310284 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum interval rat. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals. diff --git a/theories/charge.v b/theories/charge.v index 7f1a4f6b12..c1f2626d9e 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/convex.v b/theories/convex.v index 13d8f6aeb2..bd38565887 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrint ssrnum interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrint ssrnum interval. From mathcomp Require Import interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/derive.v b/theories/derive.v index 440a1497e2..18a80fa3df 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum matrix interval poly. From mathcomp Require Import sesquilinear. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/ereal.v b/theories/ereal.v index 1b206b7cee..7953aed0a6 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -5,7 +5,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 4bbcd61a9f..6848111cf1 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -1,5 +1,5 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals ereal topology normedtype sequences. From mathcomp Require Import measure lebesgue_measure. diff --git a/theories/esum.v b/theories/esum.v index a25e061a86..e1bca2c1e6 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrnum finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum finmap. 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. diff --git a/theories/exp.v b/theories/exp.v index e3a5271069..84e14e84ab 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/ftc.v b/theories/ftc.v index b83b6a397f..f87fd7146e 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 08db6e606c..4a6a2937cc 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 5f57d13718..3170422435 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval 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 topology tvs normedtype sequences real_interval. diff --git a/theories/hoelder.v b/theories/hoelder.v index 1b9d045c96..9f72d5a457 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp interval_inference. diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index 3b739b1492..c99f95e301 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals topology. From mathcomp Require Import function_spaces wedge_sigT. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index d9f999083e..526959b7aa 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. diff --git a/theories/kernel.v b/theories/kernel.v index 2eaa9643c5..d5394f83bc 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. diff --git a/theories/landau.v b/theories/landau.v index fcb35f7c62..2955f5a233 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum. +From mathcomp Require Import all_ssreflect_compat 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. diff --git a/theories/lebesgue_integral_theory/giry.v b/theories/lebesgue_integral_theory/giry.v index 3d369c65cc..8a3a17888a 100644 --- a/theories/lebesgue_integral_theory/giry.v +++ b/theories/lebesgue_integral_theory/giry.v @@ -1,5 +1,5 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra boolp classical_sets. +From mathcomp Require Import all_ssreflect_compat all_algebra boolp classical_sets. From mathcomp Require Import fsbigop functions 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 5f0fe74e9e..1879b540e0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 5f8c7703f6..f609939fbe 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 385c2ae69c..0725c1e7e0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat 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 functions. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index a7a232c7e6..077323a68e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 3622ce6a1e..16f8b325e8 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 91897623ac..fb833273dc 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index 94707803b4..ab43c808cf 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a6ad41e9fb..47afa3ca37 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v index 099b5930eb..3d04d6b650 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 14da12b366..4f17ede011 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 4b9e20fe1f..3798a7fcfc 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 1bdafa94af..98951a1d9a 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 4d3ca1d3a9..1df105e1fb 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions fsbigop cardinality. From mathcomp Require Import reals ereal interval_inference topology numfun. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 422a97b530..6f3a33d91e 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. From mathcomp Require Import boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop reals ereal. diff --git a/theories/measure_theory/counting_measure.v b/theories/measure_theory/counting_measure.v index 164a39e3c1..4c5e5030e2 100644 --- a/theories/measure_theory/counting_measure.v +++ b/theories/measure_theory/counting_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import interval_inference ereal topology normedtype. From mathcomp Require Import sequences measurable_structure measure_function. diff --git a/theories/measure_theory/dirac_measure.v b/theories/measure_theory/dirac_measure.v index f9267eef01..f0e99352ba 100644 --- a/theories/measure_theory/dirac_measure.v +++ b/theories/measure_theory/dirac_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_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. diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 56c294b87d..a20242defe 100644 --- a/theories/measure_theory/measurable_function.v +++ b/theories/measure_theory/measurable_function.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 91c1e89efb..5fcf197942 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/theories/measure_theory/measurable_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index d82dee0498..2a67f58a89 100644 --- a/theories/measure_theory/measure_extension.v +++ b/theories/measure_theory/measure_extension.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. 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. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index e564c1302b..cd339b3543 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. diff --git a/theories/measure_theory/measure_negligible.v b/theories/measure_theory/measure_negligible.v index f3d1511d94..a0146ac3ea 100644 --- a/theories/measure_theory/measure_negligible.v +++ b/theories/measure_theory/measure_negligible.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality reals. diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 1ad06c84f5..9dbcb5802a 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality reals. From mathcomp Require Import interval_inference ereal topology normedtype. From mathcomp Require Import measurable_structure measure_function dirac_measure. diff --git a/theories/normedtype_theory/complete_normed_module.v b/theories/normedtype_theory/complete_normed_module.v index 73d59feff8..c35a24e670 100644 --- a/theories/normedtype_theory/complete_normed_module.v +++ b/theories/normedtype_theory/complete_normed_module.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum. From mathcomp Require Import boolp classical_sets interval_inference reals. From mathcomp Require Import topology tvs pseudometric_normed_Zmodule. From mathcomp Require Import normed_module. diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v index db2bca5164..a6ba8dc4b4 100644 --- a/theories/normedtype_theory/ereal_normedtype.v +++ b/theories/normedtype_theory/ereal_normedtype.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum interval. +From mathcomp Require Import all_ssreflect_compat 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. diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 9d8e502c37..165e549d2b 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum matrix interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum matrix interval. From mathcomp Require Import boolp classical_sets interval_inference reals. From mathcomp Require Import topology function_spaces prodnormedzmodule tvs. From mathcomp Require Import pseudometric_normed_Zmodule normed_module. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9bf04bb6e3..a564b3525d 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean rat interval zmodp vector. From mathcomp Require Import fieldext falgebra. #[warning="-warn-library-file-internal-analysis"] diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index ef634f6da2..d2c70006e4 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 76844f9b64..d8c9ee84e9 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval interval_inference ereal reals. diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index 817fee1944..d184bd3571 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 57ff3f6031..e7b5e27a95 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/numfun.v b/theories/numfun.v index 4a678cd1d7..682438fb7b 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat 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 fsbigop. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 5bf262095e..adf90c657a 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop interval_inference. From mathcomp Require Import reals ereal topology normedtype sequences. diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index 77b0dccec9..64a6e04e7e 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index f82c2bd720..37d5579cf4 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg poly ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg poly ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v index 8ade539fa9..46cdb0cc59 100644 --- a/theories/probability_theory/binomial_distribution.v +++ b/theories/probability_theory/binomial_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v index 30c2a88a3c..fba1dc5fd0 100644 --- a/theories/probability_theory/exponential_distribution.v +++ b/theories/probability_theory/exponential_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences derive. diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index e06cb16a7a..d210b16289 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences derive. diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v index c445e654e6..206dd726f7 100644 --- a/theories/probability_theory/poisson_distribution.v +++ b/theories/probability_theory/poisson_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets reals ereal topology. From mathcomp Require Import normedtype sequences exp esum measure. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index dcbfbd40ad..e855902a40 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint poly interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint poly interval. From mathcomp Require Import archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 524a9b375a..304bbc90cf 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals interval_inference ereal topology normedtype. diff --git a/theories/realfun.v b/theories/realfun.v index f9cc0f6ea0..b2623a30f4 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean interval interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/sequences.v b/theories/sequences.v index b93e3d31cd..3d904d757b 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint. From mathcomp Require Import interval interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/showcase/pnt.v b/theories/showcase/pnt.v index b57bd3ec1f..17718529cb 100644 --- a/theories/showcase/pnt.v +++ b/theories/showcase/pnt.v @@ -1,4 +1,4 @@ -From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import classical_sets boolp topology. diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v index 801b6b9b9d..e25c747998 100644 --- a/theories/showcase/summability.v +++ b/theories/showcase/summability.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import interval zmodp. From mathcomp Require Import boolp classical_sets. From mathcomp Require Import ereal reals topology normedtype. diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index 27fedd92ec..d684beebd8 100644 --- a/theories/topology_theory/bool_topology.v +++ b/theories/topology_theory/bool_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology compact. From mathcomp Require Import discrete_topology. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index 2902527589..f72a436b39 100644 --- a/theories/topology_theory/compact.v +++ b/theories/topology_theory/compact.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v index 78a9a5aba7..c5550e92ce 100644 --- a/theories/topology_theory/connected.v +++ b/theories/topology_theory/connected.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 26207586da..ee36183075 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -1,5 +1,5 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical all_reals. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import order_topology pseudometric_structure compact. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 21f3151402..c1c1077aa5 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v index f51b940a31..432f15ea35 100644 --- a/theories/topology_theory/matrix_topology.v +++ b/theories/topology_theory/matrix_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. From mathcomp Require Import interval_inference topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v index e08ff5e9a5..b98928b607 100644 --- a/theories/topology_theory/metric_structure.v +++ b/theories/topology_theory/metric_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum matrix. From mathcomp Require Import interval_inference rat interval zmodp vector. From mathcomp Require Import fieldext falgebra archimedean finmap. #[warning="-warn-library-file-internal-analysis"] diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 952362f473..abe8989760 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology. From mathcomp Require Import discrete_topology. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index df7c804f22..5be7fb319b 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. From mathcomp Require Import order_topology matrix_topology. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index 1e8e199b13..abbf5df3cd 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure compact initial_topology. diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index c4d611b390..200b4f9e39 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import topology_structure uniform_structure. diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 56dd633458..29afdd9c31 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference topology_structure. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index 157622bd03..94eed7cc1a 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure. diff --git a/theories/topology_theory/quotient_topology.v b/theories/topology_theory/quotient_topology.v index bf5037767d..2328d0d8a8 100644 --- a/theories/topology_theory/quotient_topology.v +++ b/theories/topology_theory/quotient_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index bfd887b681..0fb7543b0a 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/theories/topology_theory/separation_axioms.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect_compat all_algebra 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. diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v index 4de744f871..f33ce39d00 100644 --- a/theories/topology_theory/sigT_topology.v +++ b/theories/topology_theory/sigT_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import topology_structure compact subspace_topology. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 12bf5c5752..03f028ea76 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure uniform_structure compact. From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology. diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index b9cb8bc6bc..6b05822640 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/theories/topology_theory/subtype_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import reals topology_structure uniform_structure compact. From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology subspace_topology. diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v index 9cbc113004..73ac80336f 100644 --- a/theories/topology_theory/supremum_topology.v +++ b/theories/topology_theory/supremum_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. From mathcomp Require Import topology_structure uniform_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 232b04c149..7eb8bbeae1 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra finmap all_classical. From mathcomp Require Export filter. (**md**************************************************************************) diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 6e7fc18006..fb34a56025 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. From mathcomp Require Import topology_structure. (**md**************************************************************************) diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 07f584dad0..667e33095f 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. diff --git a/theories/trigo.v b/theories/trigo.v index 3b3eaf2822..3c9d7388ba 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. diff --git a/theories/tvs.v b/theories/tvs.v index 82daf0d9af..ce837d6f74 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg ssrnum vector. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import set_interval reals interval_inference. From mathcomp Require Import topology function_spaces. From 6f56e9949a4e840fedb5cd19e544c0ecc1fbfe1f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Feb 2026 11:43:14 +0100 Subject: [PATCH 2/2] Compat with Rocq (without coq shim) --- Makefile.common | 10 ----- coq-mathcomp-analysis-stdlib.opam | 12 ++---- coq-mathcomp-analysis.opam | 14 ++----- coq-mathcomp-classical.opam | 17 ++------ coq-mathcomp-experimental-reals.opam | 15 ++----- coq-mathcomp-reals-stdlib.opam | 13 ++---- coq-mathcomp-reals.opam | 11 ++--- rocq-mathcomp-analysis-stdlib.opam | 42 +++++++++++++++++++ rocq-mathcomp-analysis.opam | 60 +++++++++++++++++++++++++++ rocq-mathcomp-classical.opam | 51 +++++++++++++++++++++++ rocq-mathcomp-experimental-reals.opam | 44 ++++++++++++++++++++ rocq-mathcomp-reals-stdlib.opam | 42 +++++++++++++++++++ rocq-mathcomp-reals.opam | 41 ++++++++++++++++++ 13 files changed, 298 insertions(+), 74 deletions(-) create mode 100644 rocq-mathcomp-analysis-stdlib.opam create mode 100644 rocq-mathcomp-analysis.opam create mode 100644 rocq-mathcomp-classical.opam create mode 100644 rocq-mathcomp-experimental-reals.opam create mode 100644 rocq-mathcomp-reals-stdlib.opam create mode 100644 rocq-mathcomp-reals.opam diff --git a/Makefile.common b/Makefile.common index 4f0bdbd824..1f13153e35 100644 --- a/Makefile.common +++ b/Makefile.common @@ -28,16 +28,6 @@ COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS) BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \ | wc -l | sed 's/ *//g') -# coq version: -ifneq "$(BRANCH_coq)" "0" -COQVVV:= dev -else -COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1) -endif - -COQV:= $(shell echo $(COQVVV) | cut -d"." -f1) -COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2) - # all: --------------------------------------------------------------- all: config build diff --git a/coq-mathcomp-analysis-stdlib.opam b/coq-mathcomp-analysis-stdlib.opam index 1abd3d74a3..fa29d07716 100644 --- a/coq-mathcomp-analysis-stdlib.opam +++ b/coq-mathcomp-analysis-stdlib.opam @@ -7,17 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "A library to link real numbers from mathematical components and Stdlib" -description: """ -This package contains a library to link real numbers for -the Coq proof-assistant using the Mathematical Components library and Stdlib.""" - build: [make "-C" "analysis_stdlib" "-j%{jobs}%"] install: [make "-C" "analysis_stdlib" "install"] -depends: [ - "coq-mathcomp-analysis" { = version} - "coq-mathcomp-reals-stdlib" -] +depends: [ "rocq-mathcomp-analysis-stdlib" { = version} ] tags: [ "category:Mathematics/Real Numbers" @@ -40,3 +32,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-analysis-stdlib" diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index a0890eb504..d18cd1568b 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -7,19 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "An analysis library for mathematical components" -description: """ -This package contains a library for real analysis for -the Coq proof-assistant and using the Mathematical Components library.""" - build: [make "-C" "theories" "-j%{jobs}%"] install: [make "-C" "theories" "install"] -depends: [ - "coq-mathcomp-reals" { = version} - "coq-mathcomp-solvable" - "coq-mathcomp-field" - "coq-mathcomp-bigenough" { (>= "1.0.0") } -] +depends: [ "rocq-mathcomp-analysis" { = version} ] tags: [ "category:Mathematics/Real Calculus and Topology" @@ -58,3 +48,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-analysis" diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index dd58126243..ece6b5df70 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -7,22 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "A library for classical logic for mathematical components" -description: """ -This repository contains a library for classical logic for -the Coq proof-assistant and using the Mathematical Components library.""" - build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] -depends: [ - ("coq" {>= "8.20" & < "8.21~"} - | "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") }) - "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") } - "coq-mathcomp-fingroup" - "coq-mathcomp-algebra" - "coq-mathcomp-finmap" { (>= "2.1.0") } - "coq-hierarchy-builder" { (>= "1.8.0") } -] +depends: [ "rocq-mathcomp-classical" { = version} ] tags: [ "category:Mathematics/Logic/Classical logic" @@ -49,3 +36,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-classical" diff --git a/coq-mathcomp-experimental-reals.opam b/coq-mathcomp-experimental-reals.opam index b9053fef9d..6367c78e99 100644 --- a/coq-mathcomp-experimental-reals.opam +++ b/coq-mathcomp-experimental-reals.opam @@ -7,20 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "A library for alternative real numbers for mathematical components" -description: """ -This package contains an experiment along real numbers -made at the beginning of the MathComp-Analysis library -(which now offers the coq-mathcomp-reals package). - -Beware that this still contains a few Admitted.""" - build: [make "-C" "experimental_reals" "-j%{jobs}%"] install: [make "-C" "experimental_reals" "install"] -depends: [ - "coq-mathcomp-reals" { = version} - "coq-mathcomp-bigenough" { (>= "1.0.0") } -] +depends: [ "rocq-mathcomp-experimental-reals" { = version} ] tags: [ "category:Mathematics/Real Numbers" @@ -42,3 +31,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-experimental-reals" diff --git a/coq-mathcomp-reals-stdlib.opam b/coq-mathcomp-reals-stdlib.opam index 088e50991b..4825e9e0c3 100644 --- a/coq-mathcomp-reals-stdlib.opam +++ b/coq-mathcomp-reals-stdlib.opam @@ -7,18 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "A library to link real numbers from mathematical components and Stdlib" -description: """ -This package contains a library to link real numbers for -the Coq proof-assistant using the Mathematical Components library and Stdlib.""" - build: [make "-C" "reals_stdlib" "-j%{jobs}%"] install: [make "-C" "reals_stdlib" "install"] -depends: [ - ("coq" {< "8.21~"} - | "rocq-stdlib" { (>= "9.0" & < "9.1~") | (= "dev") }) - "coq-mathcomp-reals" { = version} -] +depends: [ "rocq-mathcomp-reals-stdlib" { = version} ] tags: [ "category:Mathematics/Real Numbers" @@ -40,3 +31,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-reals-stdlib" diff --git a/coq-mathcomp-reals.opam b/coq-mathcomp-reals.opam index e718a176e6..644fd22197 100644 --- a/coq-mathcomp-reals.opam +++ b/coq-mathcomp-reals.opam @@ -7,16 +7,9 @@ dev-repo: "git+https://github.com/math-comp/analysis.git" bug-reports: "https://github.com/math-comp/analysis/issues" license: "CECILL-C" -synopsis: "A library for real numbers for mathematical components" -description: """ -This package contains a library for real numbers for -the Coq proof-assistant and using the Mathematical Components library.""" - build: [make "-C" "reals" "-j%{jobs}%"] install: [make "-C" "reals" "install"] -depends: [ - "coq-mathcomp-classical" { = version} -] +depends: [ "rocq-mathcomp-reals" { = version} ] tags: [ "category:Mathematics/Real Numbers" @@ -39,3 +32,5 @@ authors: [ "Pierre-Yves Strub" "Laurent Théry" ] + +synopsis: "Compatibility package for rocq-mathcomp-reals" diff --git a/rocq-mathcomp-analysis-stdlib.opam b/rocq-mathcomp-analysis-stdlib.opam new file mode 100644 index 0000000000..21f98df416 --- /dev/null +++ b/rocq-mathcomp-analysis-stdlib.opam @@ -0,0 +1,42 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library to link real numbers from mathematical components and Stdlib" +description: """ +This package contains a library to link real numbers for +the Coq proof-assistant using the Mathematical Components library and Stdlib.""" + +build: [make "-C" "analysis_stdlib" "-j%{jobs}%"] +install: [make "-C" "analysis_stdlib" "install"] +depends: [ + "rocq-mathcomp-analysis" { = version} + "rocq-mathcomp-reals-stdlib" +] + +tags: [ + "category:Mathematics/Real Numbers" + "category:Mathematics/Real Calculus and Topology" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.reals_stdlib" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/rocq-mathcomp-analysis.opam b/rocq-mathcomp-analysis.opam new file mode 100644 index 0000000000..d21d84c4c7 --- /dev/null +++ b/rocq-mathcomp-analysis.opam @@ -0,0 +1,60 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "An analysis library for mathematical components" +description: """ +This package contains a library for real analysis for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "theories" "-j%{jobs}%"] +install: [make "-C" "theories" "install"] +depends: [ + "rocq-mathcomp-reals" { = version} + "rocq-mathcomp-solvable" + "rocq-mathcomp-field" + "rocq-mathcomp-bigenough" { (>= "1.0.0") } +] + +tags: [ + "category:Mathematics/Real Calculus and Topology" + "keyword:analysis" + "keyword:Cantor" + "keyword:topology" + "keyword:real numbers" + "keyword:sequence" + "keyword:convexity" + "keyword:Landau notation" + "keyword:logarithm" + "keyword:sin" + "keyword:cos" + "keyword:tangent" + "keyword:trigonometric function" + "keyword:exponential" + "keyword:differentiation" + "keyword:derivative" + "keyword:measure theory" + "keyword:integration" + "keyword:Lebesgue" + "keyword:probability" + "logpath:mathcomp.analysis" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/rocq-mathcomp-classical.opam b/rocq-mathcomp-classical.opam new file mode 100644 index 0000000000..fad69a3f4e --- /dev/null +++ b/rocq-mathcomp-classical.opam @@ -0,0 +1,51 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for classical logic for mathematical components" +description: """ +This repository contains a library for classical logic for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "classical" "-j%{jobs}%"] +install: [make "-C" "classical" "install"] +depends: [ + ("coq" {>= "8.20" & < "8.21~"} + | "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") }) + "rocq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") } + "rocq-mathcomp-fingroup" + "rocq-mathcomp-algebra" + "rocq-mathcomp-finmap" { (>= "2.1.0") } + "rocq-hierarchy-builder" { (>= "1.8.0") } +] + +tags: [ + "category:Mathematics/Logic/Classical logic" + "keyword:classical logic" + "keyword:logic" + "keyword:sets" + "keyword:set theory" + "keyword:function" + "keyword:cardinal" + "keyword:filter" + "logpath:mathcomp.classical" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/rocq-mathcomp-experimental-reals.opam b/rocq-mathcomp-experimental-reals.opam new file mode 100644 index 0000000000..2864233894 --- /dev/null +++ b/rocq-mathcomp-experimental-reals.opam @@ -0,0 +1,44 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for alternative real numbers for mathematical components" +description: """ +This package contains an experiment along real numbers +made at the beginning of the MathComp-Analysis library +(which now offers the coq-mathcomp-reals package). + +Beware that this still contains a few Admitted.""" + +build: [make "-C" "experimental_reals" "-j%{jobs}%"] +install: [make "-C" "experimental_reals" "install"] +depends: [ + "rocq-mathcomp-reals" { = version} + "rocq-mathcomp-bigenough" { (>= "1.0.0") } +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.experimental_reals" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/rocq-mathcomp-reals-stdlib.opam b/rocq-mathcomp-reals-stdlib.opam new file mode 100644 index 0000000000..d3c1c81276 --- /dev/null +++ b/rocq-mathcomp-reals-stdlib.opam @@ -0,0 +1,42 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library to link real numbers from mathematical components and Stdlib" +description: """ +This package contains a library to link real numbers for +the Coq proof-assistant using the Mathematical Components library and Stdlib.""" + +build: [make "-C" "reals_stdlib" "-j%{jobs}%"] +install: [make "-C" "reals_stdlib" "install"] +depends: [ + ("coq" {< "8.21~"} + | "rocq-stdlib" { (>= "9.0" & < "9.1~") | (= "dev") }) + "rocq-mathcomp-reals" { = version} +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "logpath:mathcomp.reals_stdlib" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] diff --git a/rocq-mathcomp-reals.opam b/rocq-mathcomp-reals.opam new file mode 100644 index 0000000000..ce6f2ae563 --- /dev/null +++ b/rocq-mathcomp-reals.opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " +version: "dev" + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for real numbers for mathematical components" +description: """ +This package contains a library for real numbers for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "reals" "-j%{jobs}%"] +install: [make "-C" "reals" "install"] +depends: [ + "rocq-mathcomp-classical" { = version} +] + +tags: [ + "category:Mathematics/Real Numbers" + "keyword:real numbers" + "keyword:reals" + "keyword:extended real numbers" + "logpath:mathcomp.reals" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +]