Adapt to https://github.com/math-comp/math-comp/pull/1354

.github/workflows/docker-action.yml

@@ -17,9 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp-dev:coq-8.19'

README.md

@@ -26,7 +26,7 @@ order theory of real closed field, through quantifier elimination.
 - License: [CeCILL-B](CECILL-B)
 - Compatible Coq versions: Coq 8.18 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
   - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)

coq-mathcomp-real-closed.opam

@@ -23,7 +23,7 @@ install: [make "install"]
 depends: [
   ("coq" {>= "8.18" & < "8.21~"}
   | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
-  "coq-mathcomp-ssreflect" {>= "2.1"}
+  "coq-mathcomp-ssreflect" {>= "2.3"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
   "coq-mathcomp-bigenough" {>= "1.0.0"}

meta.yml

@@ -43,11 +43,7 @@ supported_coq_versions:
   opam: '{>= "8.18"}'
 
 tested_coq_opam_versions:
-- version: '2.1.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.19'
+- version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
@@ -65,9 +61,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "2.1"}'
+    version: '{>= "2.3"}'
   description: |-
-    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-

theories/cauchyreals.v

@@ -562,7 +562,7 @@
 Proof. by case: x. Qed.
 
 Definition cauchymod :=
   nosimpl (fun (x : creal) => let: CReal _ m := x in projT1 m).
 
 Lemma cauchymodP (x : creal) eps i j : 0 < eps ->
   (cauchymod x eps <= i)%N -> (cauchymod x eps <= j)%N -> `|x i - x j| < eps.
@@ -885,7 +885,7 @@
 Qed.
 
 Definition ubound (x : creal) := 
   nosimpl (let: exist2 b _ _ := ubound_subproof x in b).
 
 Lemma uboundP (x : creal) i : `|x i| <= ubound x.
 Proof. by rewrite /ubound; case: ubound_subproof. Qed.
@@ -1558,8 +1558,7 @@
 
 Definition horner2_creal (p : {poly {poly F}}) (x y : creal) :=
   CReal (horner2_crealP p x y).
-Notation "p .[ x , y ]" := (horner2_creal p x y)
-  (at level 2, left associativity) : creal_scope.
+Notation "p .[ x , y ]" := (horner2_creal p x y) : creal_scope.
 
 Lemma root_monic_from_neq0 (p : {poly F}) (x : creal) :
   p.[x] == 0 -> ((lead_coef p) ^-1 *: p).[x] == 0.
@@ -1662,8 +1661,7 @@
 Notation "x_neq0 ^-1" := (inv_creal x_neq0) : creal_scope.
 Notation "x / y_neq0" := (x * (y_neq0 ^-1))%CR : creal_scope.
 Notation "p .[ x ]" := (horner_creal p x) : creal_scope.
-Notation "p .[ x , y ]" := (horner2_creal p x y)
-  (at level 2, left associativity) : creal_scope.
+Notation "p .[ x , y ]" := (horner2_creal p x y) : creal_scope.
 Notation "x ^+ n" := (exp_creal x n) : creal_scope.
 
 Notation "`| x |" := (norm_creal x) : creal_scope.