From 18a22705cc116c69464bdef35ad530385c11afa6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 19 Jul 2025 15:34:53 +0900 Subject: [PATCH 1/2] fixes #1687 --- coq-mathcomp-classical.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: [ From f9d96c859dc89794b02f40c558491f5db976bb8e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 19 Jul 2025 15:39:05 +0900 Subject: [PATCH 2/2] fix other mentions of HB 1.7.0 --- INSTALL.md | 2 +- README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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