compatibility with Coq 8.21 and later

.github/workflows/docker-action.yml

@@ -19,6 +19,7 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp-dev:coq-dev'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.17'

README.md

@@ -52,7 +52,7 @@ of said algorithm.
 - Coq-community maintainer(s):
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.16 to 8.20
+- Compatible Coq versions: 8.16 or later
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later

coq-comp-dec-modal.opam

@@ -32,7 +32,7 @@ of said algorithm.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.21"}
+  "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-hierarchy-builder" {>= "1.6.0"}
 ]

meta.yml

@@ -52,10 +52,12 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.16 to 8.20
-  opam: '{>= "8.16" & < "8.21"}'
+  text: 8.16 or later
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'

theories/CTL/agreement.v

@@ -140,19 +140,19 @@ Section Paths.
   Lemma dmAU (xm : XM) w : ~ cAU R P Q w -> cER R (PredC P) (PredC Q) w.
   Proof.
     move: w. cofix dmAU => w Hw.
-    have nQw: (~ Q w). move => c. apply Hw. exact: AU0.
+    have @nQw : (~ Q w). move => c. apply Hw. exact: AU0.
     case: (xm (P w)) => [pw|nPw]; last exact: ER0.
-    suff {dmAU} [v v1 v2] : exists2 v, R w v & ~ cAU R P Q v.
+    have @ [v v1 v2] : exists2 v, R w v & ~ cAU R P Q v; last first.
       apply: ERs v1 _. exact: nQw. exact: dmAU.
-    apply: (dn xm) => C. apply: Hw. apply: AUs pw _ => v wv. 
+    apply: (dn xm) => C {nQw}. apply: Hw. apply: AUs pw _ => v wv.
     apply: (dn xm) => C'. apply: C. by exists v.
   Qed.
 
   Lemma dmAR (xm : XM) w : ~ cAR R P Q w -> cEU R (PredC P) (PredC Q) w.
   Proof.
     move => H. apply: (dn xm) => C. apply: H. 
     move: w C. cofix dmAR => w Hw.
-    have Qw : Q w. apply: (dn xm) => H. apply Hw. exact: EU0.
+    have @Qw : Q w. apply: (dn xm) => H. apply Hw. exact: EU0.
     case: (xm (P w)) => [Pw|nPw]; first exact: AR0.
     apply: ARs Qw _ => v wv. apply: dmAR => C. apply: Hw. exact: EUs C.
   Qed.
@@ -340,7 +340,7 @@ Lemma AR3_0 : cAR (@trans M3) (eval (fV 0)) (eval (fV 1)) ord0.
 Proof.
   cofix AR3_0. apply: ARs; first done. 
   case. case => [|[|n]] i. 
-  - suff ->: Ordinal i = ord0. move => _. exact: AR3_0. 
+  - have @ ->: Ordinal i = ord0; last first. move => _. exact: AR3_0.
       congr Ordinal. exact: eq_irrelevance.
   - move => _. apply: AR0 => //. 
   - move => H. case: notF. exact: contraTT H.