update meta & opam & docker

math-comp · Jul 8, 2022 · 82361f6 · 82361f6
1 parent 8a7fea2
commit 82361f6
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 10 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -22,6 +22,9 @@ jobs:
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-dev'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.14'
           - 'mathcomp/mathcomp-dev:coq-8.15'
           - 'mathcomp/mathcomp-dev:coq-dev'

diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
@@ -19,11 +19,11 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev") }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev") }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev") }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
   "coq-hierarchy-builder" { (>= "1.2.0") }

diff --git a/meta.yml b/meta.yml
@@ -63,6 +63,12 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-dev'
   repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.14'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.15'
@@ -73,27 +79,27 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp fingroup 1.13 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp algebra 1.13 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp solvable 1.13 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
+    version: '{ (>= "1.13.0" & < "1.16~") | (= "dev") }'
   description: |-
     [MathComp field 1.13 or later](https://math-comp.github.io)
 - opam: