Adapt to https://github.com/rocq-prover/rocq/pull/21849

.github/workflows/docker-action.yml

@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'

.nix/config.nix

@@ -140,13 +140,5 @@
     }; coqPackages = common-bundles // {
       coq.override.version = "9.0";
     }; };
-    "coq-8.20".coqPackages = common-bundles // {
-      coq.override.version = "8.20";
-      coq-elpi.override.version = "2.5.0";
-      coq-elpi.override.elpi-version = "2.0.7";
-      hierarchy-builder.override.version = "1.8.1";
-      mathcomp.override.version = "2.3.0";
-      mathcomp-apery.job = false;
-    };
   };
 }

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"3b7baf61aa95441d62332d7fdad562a61a125f80"
+"b777049f817b9846b0de82a7247c833e0c59feb6"

README.md

@@ -44,7 +44,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
   - Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril))
   - Pierre Roux ([**@proux01**](https://github.com/proux01))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.20 or later (use releases for other Coq versions)
+- Compatible Rocq versions: 9.0 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [Bignums](https://github.com/coq/bignums) same version as Coq
   - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 2.4.1 or later

coq-coqeal.opam

@@ -21,7 +21,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.20" & < "9.1~") | (= "dev")}
+  "coq" {(>= "9.0" & < "9.2~") | (= "dev")}
   "coq-bignums" 
   "coq-elpi" {>= "2.4.1" | = "dev"}
   "coq-hierarchy-builder" {>= "1.4.0"}

meta.yml

@@ -76,8 +76,8 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.20 or later (use releases for other Coq versions)
-  opam: '{(>= "8.20" & < "9.1~") | (= "dev")}'
+  text: 9.0 or later (use releases for other Rocq versions)
+  opam: '{(>= "9.0" & < "9.2~") | (= "dev")}'
 
 dependencies:
 - opam:
@@ -115,12 +115,8 @@ dependencies:
     [MathComp real-closed](https://math-comp.github.io) 2.0 or later
 
 tested_coq_opam_versions:
-- version: '2.3.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.20'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 

refinements/binrat.v

@@ -353,7 +353,7 @@ End Zint.
 (** ** Link between [bigQ] (Coq standard lib) and [rat] (Mathcomp) *)
 Section binrat_theory.
 
-Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *)
+Arguments refines A%_type B%_type R%_rel _ _. (* Fix a scope issue with refines *)
 
 (** *** Conversion from [bigQ] to [rat] *)
 Program Definition bigQ2rat_def (bq : bigQ) :=

refinements/multipoly.v

@@ -30,7 +30,7 @@ Import Refinements.Op.
 Local Open Scope ring_scope.
 
 (** BEGIN FIXME this is redundant with PR CoqEAL/CoqEAL#3 *)
-Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *)
+Arguments refines A%_type B%_type R%_rel _ _. (* Fix a scope issue with refines *)
 
 #[export] Hint Resolve nil_R : core.
 (** END FIXME this is redundant with PR CoqEAL/CoqEAL#3 *)

refinements/refinements.v

@@ -25,7 +25,7 @@ Section refinements.
 Fact refines_key : unit. Proof. done. Qed.
 Class refines A B (R : A -> B -> Type) (m : A) (n : B) :=
   refines_rel : (locked_with refines_key R) m n.
-Arguments refines A B R%rel m n.
+Arguments refines A B R%_rel m n.
 
 Lemma refinesE A B (R : A -> B -> Type) : refines R = R.
 Proof. by rewrite /refines unlock. Qed.
@@ -50,7 +50,7 @@ Fact composable_lock : unit. Proof. done. Qed.
 Class composable A B C
   (rAB : A -> B -> Type) (rBC : B -> C -> Type) (rAC : A -> C -> Type) :=
   Composable : locked_with composable_lock (rAB \o rBC <= rAC).
-Arguments composable A B C rAB%rel rBC%rel rAC%rel.
+Arguments composable A B C rAB%_rel rBC%_rel rAC%_rel.
 
 Lemma composableE A B C
  (rAB : A -> B -> Type) (rBC : B -> C -> Type) (rAC : A -> C -> Type) :
@@ -207,7 +207,7 @@ Qed.
 
 End refinements.
 
-Arguments refines [A B]%type R%rel m n.
+Arguments refines [A B]%_type R%_rel m n.
 Arguments refinesP {T T' R x y} _.
 
 #[export] Hint Mode refines - - - + - : typeclass_instances.

refinements/seqmx_complements.v

@@ -16,7 +16,7 @@ Import Refinements.Op.
 
 (** * Extra material about CoqEAL *)
 
-Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *)
+Arguments refines A%_type B%_type R%_rel _ _. (* Fix a scope issue with refines *)
 
 Arguments refinesP {T T' R x y} _.
 

theory/stronglydiscrete.v

@@ -62,7 +62,7 @@ Section IdealTheory.
 Definition subid m n (I : 'cV[R]_m) (J : 'cV[R]_n) : bool :=
   [forall i, member (I i 0) J].
 
-Arguments subid m%nat_scope n%nat_scope I%ideal_scope J%ideal_scope.
+Arguments subid m%_nat_scope n%_nat_scope I%_ideal_scope J%_ideal_scope.
 Prenex Implicits subid.
 Local Notation "A <= B" := (subid A B) : ideal_scope.
 Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%IS : ideal_scope.