diff --git a/README.md b/README.md
index 26a51b2..84adde7 100644
--- a/README.md
+++ b/README.md
@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/math-comp/tarjan/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/tarjan/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/tarjan/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/tarjan/actions?query=workflow:"Docker%20CI"
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -43,6 +43,7 @@ sorting with extended guarantees for acyclic graphs.
 - Additional dependencies:
   - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
 - Coq namespace: `mathcomp.tarjan`
 - Related publication(s):
   - [Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle](https://hal.inria.fr/hal-01906155) doi:[10.4230/LIPIcs.ITP.2019.13](https://doi.org/10.4230/LIPIcs.ITP.2019.13)
@@ -61,7 +62,7 @@ opam install coq-mathcomp-tarjan
 To instead build and install manually, do:
 
 ``` shell
-git clone https://github.com/math-comp/tarjan.git
+git clone https://github.com/coq-community/tarjan.git
 cd tarjan
 make   # or make -j <number-of-cores-on-your-machine> 
 make install
diff --git a/coq-mathcomp-tarjan.opam b/coq-mathcomp-tarjan.opam
index 924ebec..da0e07b 100644
--- a/coq-mathcomp-tarjan.opam
+++ b/coq-mathcomp-tarjan.opam
@@ -5,9 +5,9 @@ opam-version: "2.0"
 maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 version: "dev"
 
-homepage: "https://github.com/math-comp/tarjan"
-dev-repo: "git+https://github.com/math-comp/tarjan.git"
-bug-reports: "https://github.com/math-comp/tarjan/issues"
+homepage: "https://github.com/coq-community/tarjan"
+dev-repo: "git+https://github.com/coq-community/tarjan.git"
+bug-reports: "https://github.com/coq-community/tarjan/issues"
 license: "CECILL-B"
 
 synopsis: "Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp"
@@ -23,6 +23,7 @@ depends: [
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-fingroup" 
+  "coq-hierarchy-builder" {>= "1.4.0"}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 337cee5..c6b92f5 100644
--- a/meta.yml
+++ b/meta.yml
@@ -1,7 +1,7 @@
 ---
 fullname: Tarjan and Kosaraju
 shortname: tarjan
-organization: math-comp
+organization: coq-community
 opam_name: coq-mathcomp-tarjan
 community: true
 action: true
@@ -60,6 +60,11 @@ dependencies:
     name: coq-mathcomp-fingroup
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.4.0"}'
+  description: |-
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
 
 tested_coq_opam_versions:
 - version: '2.0.0-coq-8.17'