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/changelog.txt b/changelog.txt
index 81eff2e2..b53a6b45 100644
--- 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
index 6d20793e..a067e5fd 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..64b84ffd 100644
--- 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" }'