Compatibility with coq813 (affeldt-aist#29)

* compatibility with coq 8.13

.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

.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

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)

coq-infotheo.opam

@@ -3,6 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "Reynald Affeldt <[email protected]>"
+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~") }

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)".

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: