From 1cb9d5029624d1896d6e83d4325cb6172a771def Mon Sep 17 00:00:00 2001 From: Pierre Roux <pierre.roux@onera.fr> Date: Fri, 29 Mar 2024 14:22:07 +0100 Subject: [PATCH 1/2] Drop support for mathcomp 2.0.0 --- .github/workflows/docker-action.yml | 3 --- README.md | 8 ++++---- coq-coqeal.opam | 2 +- meta.yml | 12 +++--------- 4 files changed, 8 insertions(+), 17 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 03aa660..5cc922d 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,9 +17,6 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.0.0-coq-8.16' - - 'mathcomp/mathcomp:2.0.0-coq-8.17' - - 'mathcomp/mathcomp:2.0.0-coq-8.18' - 'mathcomp/mathcomp:2.1.0-coq-8.16' - 'mathcomp/mathcomp:2.1.0-coq-8.17' - 'mathcomp/mathcomp:2.1.0-coq-8.18' diff --git a/README.md b/README.md index c7b71dc..c413585 100644 --- a/README.md +++ b/README.md @@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Code of Conduct][conduct-shield]][conduct-link] [![Zulip][zulip-shield]][zulip-link] -[docker-action-shield]: https://github.com/coq-community/coqeal/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/coq-community/coqeal/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/coq-community/coqeal/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/coqeal/actions/workflows/docker-action.yml [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md @@ -49,8 +49,8 @@ of the ForMath EU FP7 project (2009-2013). It has two parts: - [Bignums](https://github.com/coq/bignums) same version as Coq - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later - - [MathComp ssreflect](https://math-comp.github.io) 2.0 or later - - [MathComp algebra](https://math-comp.github.io) 2.0 or later + - [MathComp ssreflect](https://math-comp.github.io) 2.1 or later + - [MathComp algebra](https://math-comp.github.io) 2.1 or later - [MathComp Multinomials](https://github.com/math-comp/multinomials) 2.0 or later - [MathComp real-closed](https://math-comp.github.io) 2.0 or later - Coq namespace: `CoqEAL` diff --git a/coq-coqeal.opam b/coq-coqeal.opam index b9c99dd..2ede11a 100644 --- a/coq-coqeal.opam +++ b/coq-coqeal.opam @@ -25,7 +25,7 @@ depends: [ "coq-bignums" "coq-paramcoq" {>= "1.1.3"} "coq-hierarchy-builder" {>= "1.4.0"} - "coq-mathcomp-ssreflect" {>= "2.0"} + "coq-mathcomp-ssreflect" {>= "2.1"} "coq-mathcomp-algebra" "coq-mathcomp-multinomials" {>= "2.0"} "coq-mathcomp-real-closed" {>= "2.0"} diff --git a/meta.yml b/meta.yml index 345761c..520ff9c 100644 --- a/meta.yml +++ b/meta.yml @@ -96,13 +96,13 @@ dependencies: [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later - opam: name: coq-mathcomp-ssreflect - version: '{>= "2.0"}' + version: '{>= "2.1"}' description: |- - [MathComp ssreflect](https://math-comp.github.io) 2.0 or later + [MathComp ssreflect](https://math-comp.github.io) 2.1 or later - opam: name: coq-mathcomp-algebra description: |- - [MathComp algebra](https://math-comp.github.io) 2.0 or later + [MathComp algebra](https://math-comp.github.io) 2.1 or later - opam: name: coq-mathcomp-multinomials version: '{>= "2.0"}' @@ -115,12 +115,6 @@ dependencies: [MathComp real-closed](https://math-comp.github.io) 2.0 or later tested_coq_opam_versions: -- version: '2.0.0-coq-8.16' - repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.17' - repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.18' - repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.16' repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.17' From 5c90833b1ef4602a749d746fbaef6670ed06d437 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi <pi8027@gmail.com> Date: Fri, 29 Mar 2024 13:30:43 +0100 Subject: [PATCH 2/2] Adapt to math-comp/math-comp#1190 --- refinements/examples/irred.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v index 576dd9d..4726e79 100644 --- a/refinements/examples/irred.v +++ b/refinements/examples/irred.v @@ -125,7 +125,7 @@ End fin_npoly. Section Irreducible. -Variable R : finIntegralDomainType. +Variable R : finIdomainType. Variable p : {poly R}. Definition irreducibleb :=