Preparing fcsl-pcm release v.2.1.0 (#49)

* Preparing fcsl-pcm release v.2.1.0 * fixed bounds * fix syntax * fixed syntax * fixed syntax * fixing dependencies * fixing dependencies * fixing dependencies * fixing bounds * fixing bounds
imdea-software · Jan 16, 2025 · a0b2563 · a0b2563
1 parent 2da486d
commit a0b2563
Show file tree

Hide file tree

Showing 18 changed files with 1,465 additions and 284 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -19,7 +19,7 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:latest-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4

diff --git a/README.md b/README.md
@@ -31,7 +31,7 @@ This library relies on propositional and functional extentionality axioms.
 - 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 or later](https://math-comp.github.io)
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp algebra](https://math-comp.github.io)
 - Coq namespace: `pcm`

diff --git a/_CoqProject b/_CoqProject
@@ -12,6 +12,7 @@ core/axioms.v
 core/prelude.v
 core/pred.v
 core/auto.v
+core/autouniq.v
 core/seqext.v
 core/slice.v
 core/uslice.v

diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam
@@ -27,7 +27,7 @@ install: [make "install"]
 depends: [
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
-  "coq-hierarchy-builder" {>= "1.7.0"}
+  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.9~") | (= "dev") }
   "coq-mathcomp-algebra" 
 ]