From 64cf675e1d1f5517b9289d2955bd26efb3dca50e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 29 Nov 2024 15:28:04 +0900
Subject: [PATCH] compact with mathcomp-analysis 1.7.0

---
 .github/workflows/docker-action.yml |  2 ++
 README.md                           |  1 +
 coq-infotheo.opam                   |  3 ++-
 information_theory/kraft.v          |  2 +-
 meta.yml                            | 11 ++++++++++-
 5 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 90e3c33a..27da9be5 100644
--- a/.github/workflows/docker-action.yml
+++ b/.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
diff --git a/README.md b/README.md
index 9cfc7bdb..32c37515 100644
--- a/README.md
+++ b/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
diff --git a/coq-infotheo.opam b/coq-infotheo.opam
index 6d20793e..20b3c972 100644
--- a/coq-infotheo.opam
+++ b/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"}
diff --git a/information_theory/kraft.v b/information_theory/kraft.v
index 4895cd4b..cb2ba05e 100644
--- a/information_theory/kraft.v
+++ b/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.
 
diff --git a/meta.yml b/meta.yml
index ac8b8431..8bed4c9b 100644
--- a/meta.yml
+++ b/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" }'