compatibility release

.github/workflows/docker-action.yml

@@ -19,6 +19,8 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

coq-monae.opam

@@ -15,15 +15,15 @@ description: """
 This Coq library contains a hierarchy of monads with their laws used
 in several examples of monadic equational reasoning."""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install_full"]
 depends: [
   "coq" { (>= "8.15" & < "8.18~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.14.0" & < "1.16~") | (= "dev")  }
+  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.5.4") }
   "coq-infotheo" { >= "0.5.0" & < "0.6~"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }

meta.yml

@@ -43,31 +43,35 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.14.0" & < "1.16~") | (= "dev")  }'
+    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam: