Merge pull request #33 from imdea-software/fix3

Author: clayrat

.github/workflows/docker-action.yml

@@ -16,7 +16,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:latest-coq-dev'
       fail-fast: false
     steps:

README.md

@@ -41,11 +41,11 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - License: [Apache-2.0](LICENSE)
 - Compatible Coq versions: Coq 8.19 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect 2.2](https://math-comp.github.io)
+  - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm)
-  - [Dune](https://dune.build) 2.5 or later
+  - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `htt`
 - Related publication(s):
   - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331)

coq-htt-core.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "[email protected]"
-version: "dev"
+version: "2.0.1"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -35,7 +35,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }

coq-htt.opam

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 maintainer: "[email protected]"
-version: "dev"
+version: "2.0.1"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -32,7 +32,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }

meta.yml

@@ -72,7 +72,7 @@ maintainers:
 
 opam-file-maintainer: [email protected]
 
-opam-file-version: dev
+opam-file-version: 2.0.1
 
 license:
   fullname: Apache-2.0
@@ -86,17 +86,17 @@ supported_coq_versions:
 tested_coq_opam_versions:
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.20'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 - version: 'latest-coq-dev'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 2.2](https://math-comp.github.io)
+    [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-