diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 663a2b3d..93a635e4 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,8 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2
diff --git a/.travis.yml b/.travis.yml
index e326e6d3..b9234e67 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -14,8 +14,7 @@ env:
   - NJOBS="2"
   - CONTRIB_NAME="infotheo"
   matrix:
-  - DOCKERIMAGE="mathcomp/mathcomp:1.12.0-coq-8.11"
-  - DOCKERIMAGE="mathcomp/mathcomp:1.12.0-coq-8.12"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.12.0-coq-8.13"
 
 install: |
   # Prepare the COQ container
diff --git a/README.md b/README.md
index 0a0ea2eb..aa8c3505 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ information theory, and linear error-correcting codes.
   - Takafumi Saikawa, Nagoya U.
   - Naruomi Obata, Titech (M2)
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.11 to 8.12
+- Compatible Coq versions: Coq 8.13
 - Additional dependencies:
   - [MathComp ssreflect 1.12](https://math-comp.github.io)
   - [MathComp fingroup 1.12](https://math-comp.github.io)
diff --git a/coq-infotheo.opam b/coq-infotheo.opam
index 3e2eead1..ce932e1d 100644
--- a/coq-infotheo.opam
+++ b/coq-infotheo.opam
@@ -3,6 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
+version: "dev"
 
 homepage: "https://github.com/affeldt-aist/infotheo"
 dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
@@ -20,7 +21,7 @@ build: [
   ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.11" & < "8.13~") | (= "dev") }
+  "coq" { (>= "8.13" & < "8.14~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") }
   "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") }
diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v
index d717dd47..d47f3cc8 100644
--- a/ecc_modern/ldpc_algo.v
+++ b/ecc_modern/ldpc_algo.v
@@ -171,7 +171,7 @@ Extract Inlined Constant R1 => "1.".
 Extract Constant RbaseSymbolsImpl.R => "float".
 Extract Constant RbaseSymbolsImpl.R0 => "0.".
 Extract Constant RbaseSymbolsImpl.R1 => "1.".
-Extract Constant ConstructiveCauchyReals.CReal => "float".
+Extract Inductive ConstructiveCauchyReals.CReal => "float" ["assert false"].
 Extract Constant ClassicalDedekindReals.DReal => "float".
 Extract Constant ClassicalDedekindReals.DRealRepr => "(fun x -> x)".
 Extract Constant ClassicalDedekindReals.DRealAbstr => "(fun x -> x)".
diff --git a/meta.yml b/meta.yml
index 2c0ad273..dcb187b8 100644
--- a/meta.yml
+++ b/meta.yml
@@ -39,13 +39,11 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.11 to 8.12
-  opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }'
+  text: Coq 8.13
+  opam: '{ (>= "8.13" & < "8.14~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.12.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.12'
+- version: '1.12.0-coq-8.13'
   repo: 'mathcomp/mathcomp'
 
 dependencies: