bump fcsl-pcm

imdea-software · Nov 11, 2022 · 2cb50b5 · 2cb50b5
1 parent 77438ed
commit 2cb50b5
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/README.md b/README.md
@@ -42,7 +42,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - Additional dependencies:
   - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
-  - [FCSL-PCM 1.6](https://github.com/imdea-software/fcsl-pcm)
+  - [FCSL-PCM 1.7](https://github.com/imdea-software/fcsl-pcm)
 - 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)

diff --git a/coq-htt.opam b/coq-htt.opam
@@ -37,7 +37,7 @@ depends: [
   "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-fingroup" 
-  "coq-fcsl-pcm" { (>= "1.6.0" & < "1.7~") | (= "dev") }
+  "coq-fcsl-pcm" { (>= "1.7.0" & < "1.8~") | (= "dev") }
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -78,9 +78,9 @@ dependencies:
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-fcsl-pcm
-    version: '{ (>= "1.6.0" & < "1.7~") | (= "dev") }'
+    version: '{ (>= "1.7.0" & < "1.8~") | (= "dev") }'
   description: |-
-    [FCSL-PCM 1.6](https://github.com/imdea-software/fcsl-pcm)
+    [FCSL-PCM 1.7](https://github.com/imdea-software/fcsl-pcm)
 
 namespace: htt