make dependency on Hierarchy Builder explicit in opam and README.md (#48

)
imdea-software · Dec 22, 2024 · 2da486d · 2da486d
1 parent 42f4e0e
commit 2da486d
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -32,6 +32,7 @@ This library relies on propositional and functional extentionality axioms.
 - Compatible Coq versions: Coq 8.19 to 8.20
 - Additional dependencies:
   - [MathComp ssreflect 2.2](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`
 - Related publication(s): none

diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam
@@ -27,6 +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-mathcomp-algebra" 
 ]
 

diff --git a/meta.yml b/meta.yml
@@ -57,6 +57,11 @@ dependencies:
     version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.2](https://math-comp.github.io)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.7.0"}'
+  description: |-
+    [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-algebra
   description: |-