Drop Coq 8.17 support to be compatible with coq-dev (8.20)

.github/workflows/docker-action.yml

@@ -20,17 +20,11 @@ jobs:
           - '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'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
           - 'mathcomp/mathcomp:2.0.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}

README.md

@@ -47,12 +47,12 @@ axiomatization of graph isomorphism).
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
   - Damien Pous ([**@damien-pous**](https://github.com/damien-pous))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.16 or later
+- Compatible Coq versions: 8.18 or later
 - Additional dependencies:
   - MathComp's [SSReflect library](https://math-comp.github.io), version 2.0 or later
   - MathComp's [Algebra library](https://math-comp.github.io)
   - MathComp's [finmap library](https://github.com/math-comp/finmap)
-  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.4.0 or later
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.5.0 or later
   - Gonthier's [formal proof](https://github.com/coq-community/fourcolor) of the Four-Color Theorem (optional dependency)
 - Coq namespace: `GraphTheory`
 - Related publication(s):

coq-graph-theory-planar.opam

@@ -16,7 +16,7 @@ as part of the Coq proof of the Four-Color Theorem."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.5"}
-  "coq" {>= "8.16"}
+  "coq" {>= "8.18"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-graph-theory" {= version}
   "coq-fourcolor"

coq-graph-theory.opam

@@ -16,11 +16,11 @@ from the literature (e.g., Menger's Theorem and Hall's Marriage Theorem)."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.5"}
-  "coq" {>= "8.16"}
+  "coq" {>= "8.18"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-finmap" 
-  "coq-hierarchy-builder" {>= "1.4.0"}
+  "coq-hierarchy-builder" {>= "1.5.0"}
 ]
 
 tags: [

meta.yml

@@ -64,8 +64,8 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.16 or later
-  opam: '{>= "8.16"}'
+  text: 8.18 or later
+  opam: '{>= "8.18"}'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'
@@ -74,22 +74,10 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
 
 ci_cron_schedule: '25 5 * * 5'
 
@@ -106,8 +94,8 @@ dependencies:
   description: MathComp's [finmap library](https://github.com/math-comp/finmap)
 - opam:
     name: coq-hierarchy-builder
-    version: '{>= "1.4.0"}'
-  description: '[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.4.0 or later'
+    version: '{>= "1.5.0"}'
+  description: '[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.5.0 or later'
 - opam:
     name: coq-fourcolor
   description: Gonthier's [formal proof](https://github.com/coq-community/fourcolor) of the Four-Color Theorem (optional dependency)

theories/core/setoid_bigop.v

@@ -46,7 +46,7 @@ Global Existing Instance mon_eqv.
 
 Class comMonoidLaws {X:setoid} (mon0 : X) (mon2 : X -> X -> X) :=
   ComMonoidLaws { 
-      mon_of_com :> monoidLaws mon0 mon2;
+      mon_of_com :: monoidLaws mon0 mon2;
       monC : forall x y, mon2 x y ≡ mon2 y x 
     }.