Merge pull request #1852 from proux01/rocq

Compatibility with Rocq (without coq shims)

Author: proux01

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.