From 46e76ed0a6093a447055132037adcfad367cb267 Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Fri, 6 Sep 2024 16:38:05 +0200
Subject: [PATCH] update descriptions

---
 .github/workflows/docker-action.yml |  6 +++---
 README.md                           |  4 ++--
 coq-fcsl-pcm.opam                   |  4 ++--
 meta.yml                            | 14 +++++++-------
 4 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index ca566b0..464a2ad 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,9 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp-dev:latest-coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index 144da15..8016fae 100644
--- a/README.md
+++ b/README.md
@@ -29,9 +29,9 @@ This library relies on propositional and functional extentionality axioms.
   - Anton Trunov
   - Alexander Gryzlov
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.15 to 8.17
+- Compatible Coq versions: Coq 8.16 to 8.19
 - Additional dependencies:
-  - [MathComp ssreflect 1.15 to 1.17](https://math-comp.github.io)
+  - [MathComp ssreflect 2.2](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
 - Coq namespace: `pcm`
 - Related publication(s): none
diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam
index 7a125ba..239e934 100644
--- a/coq-fcsl-pcm.opam
+++ b/coq-fcsl-pcm.opam
@@ -25,8 +25,8 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.15.0" & < "1.18~") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.20~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
 ]
 
diff --git a/meta.yml b/meta.yml
index d60bbc0..f38b091 100644
--- a/meta.yml
+++ b/meta.yml
@@ -40,23 +40,23 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.15 to 8.17
-  opam: '{ (>= "8.15" & < "8.19~") | (= "dev") }'
+  text: Coq 8.16 to 8.19
+  opam: '{ (>= "8.16" & < "8.20~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.15.0-coq-8.15'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.18'
+- version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-dev'
+- version: 'latest-coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.15 to 1.17](https://math-comp.github.io)
+    [MathComp ssreflect 2.2](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-