adjust opam packages and ci for MathComp 1.18 and other changes

.github/workflows/docker-action.yml

@@ -15,6 +15,7 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
@@ -27,7 +28,6 @@ jobs:
           custom_image: ${{ matrix.image }}
           custom_script: |
             startGroup "Setup and print opam config"
-              opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
               opam config list; opam repo list; opam list
             endGroup
             startGroup "Build hydra-battles dependencies"

coq-addition-chains.opam

@@ -18,8 +18,8 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
-  "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+  "coq-paramcoq" {>= "1.1.3"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
   "coq-mathcomp-algebra"
 ]
 

coq-gaia-hydras.opam

@@ -18,9 +18,9 @@ depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
   "coq-hydra-battles" {= version}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
   "coq-mathcomp-zify" {< "2"}
-  "coq-gaia-schutte" {>= "1.14" & < "1.18~"}
+  "coq-gaia-schutte" {>= "1.14" & < "1.18"}
 ]
 
 tags: [

coq-goedel.opam

@@ -18,7 +18,7 @@ depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
   "coq-hydra-battles" {= version}
-  "coq-coqprime" {= "dev"}
+  "coq-coqprime" {>= "1.2.0"}
 ]
 
 tags: [

coq-hydra-battles.opam

@@ -19,7 +19,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
-  "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
+  "coq-equations" {>= "1.2"}
   "coq-zorns-lemma" {>= "10.2.0"}
   "coq-libhyps"
 ]

meta.yml

@@ -120,6 +120,8 @@ supported_coq_versions:
   opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
@@ -132,28 +134,28 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-equations
-    version: '{(>= "1.2" & < "1.4~") | (= "dev")}'
+    version: '{>= "1.2"}'
   description: |-
     [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
 - opam:
     name: coq-paramcoq
-    version: '{(>= "1.1.3" & < "1.2~") | (= "dev")}'
+    version: '{>= "1.1.3"}'
   description: |-
     [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.13.0" & < "1.18~")}'
+    version: '{>= "1.13.0" & < "1.19"}'
   description: |-
-    [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 or later
+    [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 to 1.18
 - opam:
     name: coq-mathcomp-algebra
   description: |-
     [MathComp Algebra](https://github.com/math-comp/math-comp)
 - opam:
     name: coq-gaia-schutte
-    version: '{(>= "1.14" & < "1.18~") | (= "dev")}'
+    version: '{>= "1.14" & < "1.18"}'
   description: |-
-    [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 or later
+    [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 to 1.17
 - opam:
     name: coq-mathcomp-zify
     version: '{< "2~"}'
@@ -165,7 +167,7 @@ dependencies:
     [LibHyps](https://github.com/Matafou/LibHyps)
 - opam:
     name: coq-coqprime
-    version: '{= "dev"}'
+    version: '{>= "1.2.0"}'
   description: |-
     [CoqPrime](https://github.com/thery/coqprime)
 - opam: