fix

.github/workflows/docker-action.yml

@@ -17,7 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
       fail-fast: false

README.md

@@ -32,7 +32,7 @@ information theory, and linear error-correcting codes.
   - Naruomi Obata, Titech (M2)
   - Alessandro Bruni, IT-University of Copenhagen
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.18--8.20
+- Compatible Coq versions: Coq 8.19--8.20
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

coq-infotheo.opam

@@ -21,13 +21,13 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.18" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.2.0") }
+  "coq-mathcomp-analysis" { (>= "1.5.0") }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
   "coq-interval" { >= "4.10.0"}

meta.yml

@@ -43,12 +43,10 @@ license:
 nix: true
 
 supported_coq_versions:
-  text: Coq 8.18--8.20
-  opam: '{ (>= "8.18" & < "8.21~") | (= "dev") }'
+  text: Coq 8.19--8.20
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.20'
@@ -82,7 +80,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.2.0") }'
+    version: '{ (>= "1.5.0") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:

robust/weightedmean.v

@@ -407,7 +407,7 @@ by move=> *; exact/sq_dev_ge0.
 Qed.
 
 Lemma sq_dev_max_ge0 : 0 <= sq_dev_max.
-Proof. by rewrite /sq_dev_max; apply/topology.bigmax_geP; left. Qed.
+Proof. by rewrite /sq_dev_max; apply/boolp.bigmax_geP; left. Qed.
 
 Lemma sq_dev_max_ge u : C u != 0 -> sq_dev u <= sq_dev_max.
 Proof. by move=> Cu0; rewrite /sq_dev_max; apply/le_bigmax_cond. Qed.