diff --git a/INSTALL.md b/INSTALL.md index 9049f4c3f7..c7bd107f3f 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -5,7 +5,7 @@ - [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org) - [Mathematical Components version ≥ 2.2.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap) -- [Hierarchy builder version ≥ 1.7.0](https://github.com/math-comp/hierarchy-builder) +- [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder) - [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough) These requirements can be installed in a custom way, or through diff --git a/README.md b/README.md index 20be5e33a1..44ede20c63 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol - [MathComp field 2.1.0 or later](https://math-comp.github.io) - [MathComp finmap 2.0.0](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) + - [Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder) - Coq/Rocq namespace: `mathcomp.analysis` ## Building and installation instructions diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 3f74755023..9afdf12d1d 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -21,7 +21,7 @@ depends: [ "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-finmap" { (>= "2.1.0") } - "coq-hierarchy-builder" { (>= "1.7.0") } + "coq-hierarchy-builder" { (>= "1.8.0") } ] tags: [