From 9c3e79989e361dd372bdb4d5694a09d94af331af Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 14 Jun 2021 12:08:13 +0900
Subject: [PATCH] support mca 0.3.9

---
 README.md                                     | 2 +-
 coq-infotheo.opam                             | 2 +-
 information_theory/binary_symmetric_channel.v | 4 +++-
 meta.yml                                      | 4 ++--
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 444d9624..755c3ecb 100644
--- a/README.md
+++ b/README.md
@@ -38,7 +38,7 @@ information theory, and linear error-correcting codes.
   - [MathComp algebra 1.12](https://math-comp.github.io)
   - [MathComp solvable 1.12](https://math-comp.github.io)
   - [MathComp field 1.12](https://math-comp.github.io)
-  - [MathComp analysis 0.3.{6,7}](https://github.com/math-comp/analysis)
+  - [MathComp analysis](https://github.com/math-comp/analysis)
 - Coq namespace: `infotheo`
 - Related publication(s):
   - [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2)
diff --git a/coq-infotheo.opam b/coq-infotheo.opam
index 4bc08421..589ff794 100644
--- a/coq-infotheo.opam
+++ b/coq-infotheo.opam
@@ -27,7 +27,7 @@ depends: [
   "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") }
-  "coq-mathcomp-analysis" { (>= "0.3.6") & (<= "0.3.7") }
+  "coq-mathcomp-analysis" { (>= "0.3.6") & (<= "0.3.7") & (<= "0.3.9") & (< "0.4~")}
 ]
 
 tags: [
diff --git a/information_theory/binary_symmetric_channel.v b/information_theory/binary_symmetric_channel.v
index aea1592d..493d4292 100644
--- a/information_theory/binary_symmetric_channel.v
+++ b/information_theory/binary_symmetric_channel.v
@@ -164,7 +164,9 @@ Let p_01 := Eval hnf in Prob.mk_ (ltR2W p_01').
 
 Theorem BSC_capacity : capacity (BSC.c card_A p_01) = 1 - H2 p.
 Proof.
-rewrite /capacity; set E := (fun y : R => _); set p' := Prob.mk_ (ltR2W p_01').
+rewrite /capacity /image.
+set E := (fun y : R => _).
+set p' := Prob.mk_ (ltR2W p_01').
 have has_sup_E : has_sup E.
   split.
     set d := Binary.d card_A p' (Set2.a card_A).
diff --git a/meta.yml b/meta.yml
index 7a4b3d8a..800a8d60 100644
--- a/meta.yml
+++ b/meta.yml
@@ -76,9 +76,9 @@ dependencies:
     [MathComp field 1.12](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.3.6") & (<= "0.3.7") }'
+    version: '{ (>= "0.3.6") & (<= "0.3.7") & (<= "0.3.9") & (< "0.4~")}'
   description: |-
-    [MathComp analysis 0.3.{6,7}](https://github.com/math-comp/analysis)
+    [MathComp analysis](https://github.com/math-comp/analysis)
 namespace: infotheo
 
 keywords: