From 6a3830835d07d47d77ef3d8e0c75f8837038625c Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 28 Feb 2025 11:56:10 +0100
Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1354

This drops support for mathcomp 2.1 and 2.2
---
 .github/workflows/docker-action.yml |  4 +---
 README.md                           |  2 +-
 coq-mathcomp-real-closed.opam       |  2 +-
 meta.yml                            | 10 +++-------
 theories/cauchyreals.v              |  6 ++----
 5 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index dd5a105..baefe08 100644
--- a/.github/workflows/docker-action.yml
+++ b/.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'
diff --git a/README.md b/README.md
index 673fc87..9d4ff4f 100644
--- a/README.md
+++ b/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)
diff --git a/coq-mathcomp-real-closed.opam b/coq-mathcomp-real-closed.opam
index 0d74661..40ab12f 100644
--- a/coq-mathcomp-real-closed.opam
+++ b/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"}
diff --git a/meta.yml b/meta.yml
index 08367cf..1d8ef5c 100644
--- a/meta.yml
+++ b/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: |-
diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v
index 3313029..7229b97 100644
--- a/theories/cauchyreals.v
+++ b/theories/cauchyreals.v
@@ -1558,8 +1558,7 @@ Qed.
 
 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 * y" := (mul_creal x y) : creal_scope.
 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.