From c60a24e5d65c74547e9776b565efe5f6c54fb736 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 6 Jul 2022 04:18:30 +0900
Subject: [PATCH] add mathcomp 1.16 to CI

---
 .github/workflows/docker-action.yml |  3 +++
 README.md                           |  2 +-
 coq-mathcomp-finmap.opam            |  2 +-
 meta.yml                            | 10 ++++++++--
 4 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index bc15aae..eafb957 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -25,6 +25,9 @@ jobs:
           - 'mathcomp/mathcomp:1.14.0-coq-8.13'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp-dev:coq-8.13'
           - 'mathcomp/mathcomp-dev:coq-8.14'
           - 'mathcomp/mathcomp-dev:coq-8.15'
diff --git a/README.md b/README.md
index 2840133..ae8d2de 100644
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@ which will be used to subsume notations for finite sets, eventually.
 - License: [CeCILL-B](CECILL-B)
 - Compatible Coq versions: Coq 8.13 to 8.15
 - Additional dependencies:
-  - [MathComp ssreflect 1.12 to 1.14](https://math-comp.github.io)
+  - [MathComp ssreflect 1.12 to 1.15](https://math-comp.github.io)
 - Coq namespace: `mathcomp.finmap`
 - Related publication(s): none
 
diff --git a/coq-mathcomp-finmap.opam b/coq-mathcomp-finmap.opam
index 9530c7b..86aed37 100644
--- a/coq-mathcomp-finmap.opam
+++ b/coq-mathcomp-finmap.opam
@@ -22,7 +22,7 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.15~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.16~") | (= "dev") }
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index d172db2..69c6921 100644
--- a/meta.yml
+++ b/meta.yml
@@ -51,6 +51,12 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.13'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.14'
@@ -63,9 +69,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.12.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.12.0" & < "1.16~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.12 to 1.14](https://math-comp.github.io)
+    [MathComp ssreflect 1.12 to 1.15](https://math-comp.github.io)
 
 namespace: mathcomp.finmap