coq 8.19 mathcomp 2.2.0

.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

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
 

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.

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: [

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 _ => //.

meta.yml

@@ -76,42 +76,42 @@ 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")}'
   description: |-
     [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