bump upper coq version

imdea-software · May 10, 2024 · 0a4c86f · 0a4c86f
1 parent 3dd8416
commit 0a4c86f
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 7 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,7 +17,7 @@ jobs:
  matrix:
  image:
  - 'mathcomp/mathcomp:1.17.0-coq-8.15'
- - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+ - 'mathcomp/mathcomp:1.17.0-coq-8.18'
  fail-fast: false
  steps:
  - uses: actions/checkout@v2

diff --git a/README.md b/README.md
@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/imdea-software/htt/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/imdea-software/htt/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/imdea-software/htt/actions/workflows/docker-action.yml
 
 
 

diff --git a/coq-htt-examples.opam b/coq-htt-examples.opam
@@ -33,7 +33,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
- "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
+ "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
  "coq-mathcomp-algebra" 
  "coq-mathcomp-fingroup" 

diff --git a/coq-htt.opam b/coq-htt.opam
@@ -34,7 +34,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
  "dune" {>= "2.5"}
- "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
+ "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.18~") | (= "dev") }
  "coq-mathcomp-algebra" 
  "coq-mathcomp-fingroup" 

diff --git a/meta.yml b/meta.yml
@@ -79,12 +79,12 @@ license:
 
 supported_coq_versions:
  text: Coq 8.15 to 8.17
- opam: '{ (>= "8.15" & < "8.18~") | (= "dev") }'
+ opam: '{ (>= "8.15" & < "8.19~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.17.0-coq-8.15'
  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
+- version: '1.17.0-coq-8.18'
  repo: 'mathcomp/mathcomp'
 # - version: 'coq-dev'
 # repo: 'mathcomp/mathcomp-dev'