support mca 0.3.9

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)

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: [

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).

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: