finmap is compatible with Coq 8.13

.github/workflows/coq-action.yml

@@ -21,6 +21,7 @@ jobs:
           - 'mathcomp/mathcomp:1.12.0-coq-8.10'
           - 'mathcomp/mathcomp:1.12.0-coq-8.11'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp-dev:coq-8.10'
           - 'mathcomp/mathcomp-dev:coq-8.11'
           - 'mathcomp/mathcomp-dev:coq-8.12'

README.md

@@ -20,7 +20,7 @@ which will be used to subsume notations for finite sets, eventually.
   - Cyril Cohen (initial)
   - Kazuhiko Sakaguchi
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.10 to 8.12
+- Compatible Coq versions: Coq 8.10 to 8.13
 - Additional dependencies:
   - [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io)
   - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)

coq-mathcomp-finmap.opam

@@ -18,7 +18,7 @@ which will be used to subsume notations for finite sets, eventually."""
 build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.10" & < "8.13~") | (= "dev") }
+  "coq" { (>= "8.10" & < "8.14~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.13~") | (= "dev") }
   "coq-mathcomp-bigenough" {>= "1.0.0"}
 ]

meta.yml

@@ -31,8 +31,8 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.10 to 8.12
-  opam: '{ (>= "8.10" & < "8.13~") | (= "dev") }'
+  text: Coq 8.10 to 8.13
+  opam: '{ (>= "8.10" & < "8.14~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.11.0-coq-8.10'
@@ -47,12 +47,17 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.10'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.11'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.12'
   repo: 'mathcomp/mathcomp-dev'
+# to uncomment after merging math-comp/math-comp#688
+# - version: 'coq-8.13'
+#   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'