diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index bb33989..4e12985 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,7 +17,7 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/README.md b/README.md index ecf3b3c..097ce96 100644 --- a/README.md +++ b/README.md @@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Docker CI][docker-action-shield]][docker-action-link] -[docker-action-shield]: https://github.com/thery/mathcomp-extra/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/thery/mathcomp-extra/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/thery/mathcomp-extra/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/thery/mathcomp-extra/actions/workflows/docker-action.yml @@ -66,13 +66,13 @@ A note about sorting network is available [here](https://hal.inria.fr/hal-035856 - License: [MIT License](LICENSE) - Compatible Coq versions: 8.18 or later - Additional dependencies: - - [ Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder) - - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io) - - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io) - - [MathComp algebra 2.1.0 or later](https://math-comp.github.io) - - [MathComp field 2.1.0 or later](https://math-comp.github.io) + - [ Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) + - [MathComp ssreflect 2.2.0 or later](https://math-comp.github.io) + - [MathComp fingroup 2.2.0 or later](https://math-comp.github.io) + - [MathComp algebra 2.2.0 or later](https://math-comp.github.io) + - [MathComp field 2.2.0 or later](https://math-comp.github.io) - [MathComp zify 1.5.0+2.0+8.16 or later](https://github.com/math-comp/mczify) - - [MathComp Algebra Tactics 1.2.2 or later](https://github.com/math-comp/algebra-tactics) + - [MathComp Algebra Tactics 1.2.3 or later](https://github.com/math-comp/algebra-tactics) - Coq namespace: `mathcomp-extra` - Related publication(s): none diff --git a/aks.v b/aks.v index 58fee5f..6d4d41d 100644 --- a/aks.v +++ b/aks.v @@ -684,7 +684,7 @@ Lemma is_iexp_inj (F : finFieldType) (h : {poly F}) k s {in Nbar p q (sqrtn #|M|) &, injective (fun i : 'I_ _ => inZp i : 'Z_k)}. Proof. move=> hMK hQh k_gt1 hMI hDxk1 p_gt1 pIN q_gt1 qIN pqLqh i j iIN jIN. -move=> /(congr1 val); rewrite /= {5 10}Zp_cast // => imEjm. +move=> /(congr1 val); rewrite /= [X in _ = _ %[mod X]]Zp_cast // => imEjm. have k_gt0 : 0 < k by rewrite -ltnS ltnW. pose r := map_poly (qfpoly_const hMI) ('X^i - 'X^j). suff : r == 0. diff --git a/coq-mathcomp-extra.opam b/coq-mathcomp-extra.opam index 1ab1ee1..c851164 100644 --- a/coq-mathcomp-extra.opam +++ b/coq-mathcomp-extra.opam @@ -63,13 +63,13 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {(>= "8.18")} - "coq-hierarchy-builder" {(>= "1.6.0")} - "coq-mathcomp-ssreflect" {(>= "2.1.0")} - "coq-mathcomp-fingroup" {(>= "2.1.0")} - "coq-mathcomp-algebra" {(>= "2.1.0")} - "coq-mathcomp-field" {(>= "2.1.0")} + "coq-hierarchy-builder" {(>= "1.7.0")} + "coq-mathcomp-ssreflect" {(>= "2.2.0")} + "coq-mathcomp-fingroup" {(>= "2.2.0")} + "coq-mathcomp-algebra" {(>= "2.2.0")} + "coq-mathcomp-field" {(>= "2.2.0")} "coq-mathcomp-zify" {(>= "1.5.0+2.0+8.16")} - "coq-mathcomp-algebra-tactics" {(>= "1.2.2")} + "coq-mathcomp-algebra-tactics" {(>= "1.2.3")} ] tags: [ diff --git a/digitn.v b/digitn.v index a5e7332..b5cbad1 100644 --- a/digitn.v +++ b/digitn.v @@ -155,7 +155,7 @@ Lemma Fp_exprnD (p1 p2 : {poly 'F_p}) : (p1 + p2) ^+ p = p1 ^+ p + p2 ^+ p. Proof. rewrite -[X in _ ^+ X](prednK (prime_gt0 Pp)). rewrite exprDn big_ord_recl /= subn0 mulr1 bin0 mulr1n. -rewrite big_ord_recr /bump add1n //= !prednK ?prime_gt0 //; congr (_ + _). +rewrite big_ord_recr /bump add1n //= prednK // ?prime_gt0 //; congr (_ + _). rewrite subnn binn mul1r mulr1n big1 ?add0r // => i _. have /dvdnP[k ->] : (p %| 'C(p, (0 <= i) + i))%N. apply: prime_dvd_bin Pp _ => //. diff --git a/meta.yml b/meta.yml index f17325e..793ad47 100644 --- a/meta.yml +++ b/meta.yml @@ -76,29 +76,29 @@ supported_coq_versions: dependencies: - opam: name: coq-hierarchy-builder - version: '{(>= "1.6.0")}' + version: '{(>= "1.7.0")}' description: |- - [ Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder) + [ Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) - opam: name: coq-mathcomp-ssreflect - version: '{(>= "2.1.0")}' + version: '{(>= "2.2.0")}' description: |- - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io) + [MathComp ssreflect 2.2.0 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{(>= "2.1.0")}' + version: '{(>= "2.2.0")}' description: |- - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io) + [MathComp fingroup 2.2.0 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{(>= "2.1.0")}' + version: '{(>= "2.2.0")}' description: |- - [MathComp algebra 2.1.0 or later](https://math-comp.github.io) + [MathComp algebra 2.2.0 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{(>= "2.1.0")}' + version: '{(>= "2.2.0")}' description: |- - [MathComp field 2.1.0 or later](https://math-comp.github.io) + [MathComp field 2.2.0 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-zify version: '{(>= "1.5.0+2.0+8.16")}' @@ -106,12 +106,12 @@ dependencies: [MathComp zify 1.5.0+2.0+8.16 or later](https://github.com/math-comp/mczify) - opam: name: coq-mathcomp-algebra-tactics - version: '{(>= "1.2.2")}' + version: '{(>= "1.2.3")}' description: |- - [MathComp Algebra Tactics 1.2.2 or later](https://github.com/math-comp/algebra-tactics) + [MathComp Algebra Tactics 1.2.3 or later](https://github.com/math-comp/algebra-tactics) tested_coq_opam_versions: -- version: '2.1.0-coq-8.18' +- version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' namespace: mathcomp-extra