From d57704a538f545ef99bbbfec90ec4a5945be1f9b Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 22 Dec 2024 19:24:05 +0100
Subject: [PATCH] make dependency on Hierarchy Builder explicit in opam and
 README.md

---
 README.md         | 1 +
 coq-fcsl-pcm.opam | 1 +
 meta.yml          | 5 +++++
 3 files changed, 7 insertions(+)

diff --git a/README.md b/README.md
index 70a6c74..54c4882 100644
--- 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
index dcec1f7..104d746 100644
--- 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
index 28e684d..ce4edd6 100644
--- 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: |-