Compatibility with Coq 8.20

.github/workflows/docker-action.yml

@@ -18,13 +18,14 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20'
           - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-coq-art.opam'

coq-coq-art.opam

@@ -20,7 +20,7 @@ out of over 200 exercises from the book."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.20") | (= "dev")}
+  "coq" {>= "8.16"}
 ]
 
 tags: [

meta.yml

@@ -41,10 +41,11 @@ license:
 
 supported_coq_versions:
   text: 8.16 or later (use the corresponding release for other Coq versions)
-  opam: '{(>= "8.16" & < "8.20") | (= "dev")}'
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.20'
 - version: '8.19'
 - version: '8.18'
 - version: '8.17'

tutorial_type_classes/SRC/EMonoid.v

@@ -3,25 +3,21 @@
 Set Implicit Arguments.
 Require Import Morphisms Relations.
 
-
 Class EMonoid (A:Type)(E_eq :relation  A)(dot : A->A->A)(one : A):={
-  E_rel :> Equivalence E_eq; 
-  E_dot_proper :> Proper (E_eq ==> E_eq ==> E_eq) dot; 
+  E_rel : Equivalence E_eq; 
+  E_dot_proper : Proper (E_eq ==> E_eq ==> E_eq) dot; 
   E_dot_assoc : forall x y z:A, E_eq (dot x (dot y z)) (dot (dot x y) z);
   E_one_left : forall x, E_eq (dot one  x) x;
   E_one_right : forall x, E_eq (dot x  one) x}.
+#[global] Existing Instance E_rel.
+#[global] Existing Instance E_dot_proper.
 
 Generalizable Variables A E_eq dot one.
 
-
 Fixpoint Epower `{M: EMonoid }(a:A)(n:nat) :=
   match n with 0%nat => one
              | S p => dot a (Epower a p)
   end.
 
 Class Abelian_EMonoid `(M:EMonoid ):= {
   Edot_comm : forall x y, E_eq (dot x  y)  (dot y  x)}.
-
-
-
-

tutorial_type_classes/SRC/Monoid_op_classes.v

@@ -316,13 +316,15 @@ Infix "==" := equiv (at level 70):type_scope.
 
   Open Scope M_scope.
 
-  Class EMonoid (A:Type)(E_eq :Equiv A)(E_dot : monoid_binop A)(E_one : A):={
-  E_rel :> Equivalence equiv; 
-  dot_proper :> Proper (equiv ==> equiv ==> equiv) monoid_op; 
+Class EMonoid (A:Type)(E_eq :Equiv A)(E_dot : monoid_binop A)(E_one : A) :=
+{ E_rel : Equivalence equiv; 
+  dot_proper : Proper (equiv ==> equiv ==> equiv) monoid_op; 
   E_dot_assoc : forall x y z:A,
       x * (y * z) == x * y * z;
   E_one_left : forall x, E_one * x == x;
-  E_one_right : forall x, x * E_one == x}.
+  E_one_right : forall x, x * E_one == x }.
+#[global] Existing Instance E_rel.
+#[global] Existing Instance dot_proper.
 
 Generalizable Variables E_eq E_dot E_one.
 
@@ -438,9 +440,14 @@ Module SemiRing.
 (* Overloaded notations *)
 
 Class RingOne A := ring_one : A.
+
 Class RingZero A := ring_zero : A.
-Class RingPlus A := ring_plus :> monoid_binop A.
-Class RingMult A := ring_mult :> monoid_binop A.
+
+Class RingPlus A := ring_plus : monoid_binop A.
+#[global] Existing Instance ring_plus.
+
+Class RingMult A := ring_mult : monoid_binop A.
+#[global] Existing Instance ring_mult.
 
 Infix "+" := ring_plus.
 Infix "*" := ring_mult.
@@ -461,19 +468,23 @@ Class Absorb {A} `{Equiv A} (m: A -> A -> A) (x : A) : Prop :=
   { absorb_l c : m x c = x ;
     absorb_r c : m c x = x }.
 
-Class ECommutativeMonoid `(Equiv A) (E_dot : monoid_binop A)(E_one : A):=
-  { e_commmonoid_monoid :> EMonoid equiv E_dot E_one;
-    e_commmonoid_commutative :> Commutative E_dot }.
+Class ECommutativeMonoid `(Equiv A) (E_dot : monoid_binop A)(E_one : A) :=
+  { e_commmonoid_monoid : EMonoid equiv E_dot E_one;
+    e_commmonoid_commutative : Commutative E_dot }.
+#[global] Existing Instance e_commmonoid_monoid.
+#[global] Existing Instance e_commmonoid_commutative.
 
 Class ESemiRing (A:Type) (E_eq :Equiv A) (E_plus : RingPlus A) (E_zero : RingZero A)
             (E_mult : RingMult A) (E_one : RingOne A):=
-  { add_monoid :> ECommutativeMonoid equiv ring_plus ring_zero ;
-    mul_monoid :> EMonoid equiv ring_mult ring_one ;
-    ering_dist :> Distribute ring_mult ring_plus ;
-    ering_0_mult :> Absorb ring_mult 0
+  { add_monoid : ECommutativeMonoid equiv ring_plus ring_zero ;
+    mul_monoid : EMonoid equiv ring_mult ring_one ;
+    ering_dist : Distribute ring_mult ring_plus ;
+    ering_0_mult : Absorb ring_mult 0
   }.
-
-
+#[global] Existing Instance add_monoid.
+#[global] Existing Instance mul_monoid.
+#[global] Existing Instance ering_dist.
+#[global] Existing Instance ering_0_mult.
 
 Section SemiRingTheory.