diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 928a820..1a26e6f 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 }} diff --git a/README.md b/README.md index 27e8c75..b2dffb1 100644 --- a/README.md +++ b/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): diff --git a/coq-graph-theory-planar.opam b/coq-graph-theory-planar.opam index 9e5e588..88c8b81 100644 --- a/coq-graph-theory-planar.opam +++ b/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" diff --git a/coq-graph-theory.opam b/coq-graph-theory.opam index 1f8ef53..374348d 100644 --- a/coq-graph-theory.opam +++ b/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: [ diff --git a/meta.yml b/meta.yml index 048fe4c..86a77c4 100644 --- a/meta.yml +++ b/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) diff --git a/theories/core/setoid_bigop.v b/theories/core/setoid_bigop.v index 01973b9..41ee8bb 100644 --- a/theories/core/setoid_bigop.v +++ b/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 }.