Merge pull request #33 from coq-community/compat-8.20

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.