From a7c3e041cf1ba3f629dbdc5a4c153c50371855ba Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 10 Sep 2024 00:08:31 +0200
Subject: [PATCH] try 8.20

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

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 0a615ad..cc4313b 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,8 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:latest-coq-dev'
       fail-fast: false
     steps:
diff --git a/README.md b/README.md
index 2ee61ae..70a6c74 100644
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@ This library relies on propositional and functional extentionality axioms.
   - Anton Trunov
   - Alexander Gryzlov
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.18 to 8.19
+- Compatible Coq versions: Coq 8.19 to 8.20
 - Additional dependencies:
   - [MathComp ssreflect 2.2](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam
index 46dfbb7..eedbde8 100644
--- a/coq-fcsl-pcm.opam
+++ b/coq-fcsl-pcm.opam
@@ -25,7 +25,7 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
 ]
diff --git a/meta.yml b/meta.yml
index c488bea..35a1665 100644
--- a/meta.yml
+++ b/meta.yml
@@ -40,14 +40,14 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.18 to 8.19
-  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
+  text: Coq 8.19 to 8.20
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 - version: 'latest-coq-dev'
   repo: 'mathcomp/mathcomp'