[CI] Add Coq 8.17

JasonGross · Feb 7, 2023 · b5e20bf · b5e20bf
1 parent ce1bdcf
commit b5e20bf
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -11,16 +11,20 @@ jobs:
           - mathcomp/mathcomp:1.13.0-coq-8.11
           - mathcomp/mathcomp:1.13.0-coq-8.12
           - coqorg/coq:8.13-native-ocaml-4.07 # with the coq-native opam pkg
-          - coqorg/coq:8.14-native-ocaml-4.07 # with the coq-native opam pkg
+          - coqorg/coq:8.17-native-ocaml-4.13-flambda # with the coq-native opam pkg
           - mathcomp/mathcomp:1.13.0-coq-8.13 # (without coq-native for now)
           - mathcomp/mathcomp:1.13.0-coq-8.14 # (without coq-native for now)
           - mathcomp/mathcomp:1.13.0-coq-8.15 # (without coq-native for now)
           - 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:1.15.0-coq-8.16
+          - mathcomp/mathcomp:1.16.0-coq-8.13
+          - mathcomp/mathcomp:1.16.0-coq-8.14
+          - mathcomp/mathcomp:1.16.0-coq-8.15
+          - mathcomp/mathcomp:1.16.0-coq-8.16
+          - mathcomp/mathcomp:1.16.0-coq-8.17
           - mathcomp/mathcomp-dev:coq-8.15 # (without coq-native for now)
           - mathcomp/mathcomp-dev:coq-8.16 # (without coq-native for now)
+          - mathcomp/mathcomp-dev:coq-8.17 # (without coq-native for now)
           - mathcomp/mathcomp-dev:coq-dev # (without coq-native for now)
           # the previous comments refer to https://github.com/coq/ceps/pull/48
       fail-fast: false

diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
@@ -10,7 +10,7 @@ build: [
   [ "dune" "build" "-p" name "-j" jobs ]
 ]
 depends: [
-  "coq"                    {(>= "8.10" & < "8.17~") | = "dev"}
+  "coq"                    {(>= "8.10" & < "8.18~") | = "dev"}
   "dune"                   {>= "2.8"}
   "coq-mathcomp-ssreflect" {(>= "1.13" & < "1.17~") | = "dev"}
   "coq-mathcomp-algebra"