compact with mathcomp-analysis 1.7.0 (#132)

* compact with mathcomp-analysis 1.7.0
affeldt-aist · Nov 29, 2024 · 96396c4 · 96396c4
1 parent 96bca60
commit 96396c4
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 3 deletions.
diff --git 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/changelog.txt b/changelog.txt
@@ -1,3 +1,9 @@
+-------------------
+from 0.7.4 to 0.7.5
+-------------------
+
+- compatibility with MathComp-Analysis 1.7.0 only
+
 -------------------
 from 0.7.3 to 0.7.4
 -------------------

diff --git 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
@@ -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
@@ -80,9 +80,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" }'