From b4e55704f494db5ed18afbd0f76ea16b425f35ea Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 19 Nov 2021 22:27:41 +0900
Subject: [PATCH] fix bigenough CI error

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

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")}'