Compatibility with Rocq (without coq shims)

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
 

_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

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.

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

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.

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.
 

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

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.

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.
 

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.
 

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.

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.

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

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.

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

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"

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"

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"

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"

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"

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"

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

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.
 

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.

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.

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.

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.

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

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.
 

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.

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.

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