compact with mathcomp-analysis 1.7.0

.github/workflows/docker-action.yml

@@ -19,6 +19,8 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -40,6 +40,7 @@ information theory, and linear error-correcting codes.
   - [MathComp solvable](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
   - [MathComp analysis](https://github.com/math-comp/analysis)
+  - [MathComp analysis reals standard library](https://github.com/math-comp/analysis)
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
   - MathComp algebra tactics
   - A Coq tactic for proving bounds

coq-infotheo.opam

@@ -27,7 +27,8 @@ depends: [
   "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.5.0") }
+  "coq-mathcomp-analysis" { (>= "1.7.0") }
+  "coq-mathcomp-reals-stdlib" { (>= "1.7.0) }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
   "coq-interval" { >= "4.10.0"}

information_theory/kraft.v

@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect path ssralg ssrnum.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require FunctionalExtensionality.
 Require Import ssr_ext.
 

meta.yml

@@ -51,6 +51,10 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
@@ -80,9 +84,14 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.5.0") }'
+    version: '{ (>= "1.7.0") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
+- opam:
+    name: coq-mathcomp-reals-stdlib
+    version: '{ (>= "1.7.0) }'
+  description: |-
+    [MathComp analysis reals standard library](https://github.com/math-comp/analysis)
 - opam:
     name: coq-hierarchy-builder
     version: '{ >= "1.5.0" }'