diff --git a/README.md b/README.md index c0bcb1725..f79d2df34 100644 --- a/README.md +++ b/README.md @@ -41,6 +41,7 @@ the Coq proof-assistant and using the Mathematical Components library. - [MathComp solvable 1.12 or later](https://math-comp.github.io) - [MathComp field 1.12 or later](https://math-comp.github.io) - [MathComp finmap 1.5.1](https://github.com/math-comp/finmap) + - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - [Hierarchy Builder >= 0.10.0](https://github.com/math-comp/hierarchy-builder) - Coq namespace: `mathcomp.analysis` - Related publication(s): diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index 92bfe67c4..d98210498 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -25,6 +25,7 @@ depends: [ "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.14~") | (= "dev") } "coq-mathcomp-field" { (>= "1.12.0" & < "1.14~") | (= "dev") } "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") } + "coq-mathcomp-bigenough" { (>= "1.0.0") | (= "dev") } "coq-hierarchy-builder" { (>= "0.10.0")} ] diff --git a/meta.yml b/meta.yml index 7db2b0b2b..76b2e46b0 100644 --- a/meta.yml +++ b/meta.yml @@ -104,6 +104,11 @@ dependencies: version: '{ (>= "1.5.1" & < "1.6~") | (= "dev") }' description: |- [MathComp finmap 1.5.1](https://github.com/math-comp/finmap) +- opam: + name: coq-mathcomp-bigenough + version: '{ (>= "1.0.0") | (= "dev") }' + description: |- + [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough) - opam: name: coq-hierarchy-builder version: '{ (>= "0.10.0")}'