mathcomp 2.3.0

Author: thery

.github/workflows/docker-action.yml

@@ -17,10 +17,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-twoSquare.opam'

README.md

@@ -6,8 +6,10 @@ 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/twoSquare/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/thery/twoSquare/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/thery/twoSquare/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/thery/twoSquare/actions/workflows/docker-action.yml
+
+
 
 
 
@@ -41,11 +43,11 @@ reflect
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.18 or later
+- Compatible Coq versions: 8.20 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.1 or later](https://math-comp.github.io)
-  - [MathComp field 2.1 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.3 or later](https://math-comp.github.io)
+  - [MathComp field 2.3 or later](https://math-comp.github.io)
 - Coq namespace: `twoSquare`
 - Related publication(s): none
 

coq-twoSquare.opam

@@ -41,10 +41,10 @@ reflect
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.18")}
-  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
-  "coq-mathcomp-algebra" {(>= "2.1.0")}
-  "coq-mathcomp-field" {(>= "2.1.0")}
+  "coq" {(>= "8.20")}
+  "coq-mathcomp-ssreflect" {(>= "2.3.0")}
+  "coq-mathcomp-algebra" {(>= "2.3.0")}
+  "coq-mathcomp-field" {(>= "2.3.0")}
 ]
 
 tags: [

gauss_int.v

@@ -914,7 +914,7 @@ rewrite ltnS leqn0 normGI_eq0 => /eqP->.
 by rewrite modGI0 gcdGI0.
 Qed.
 
-Lemma gcdGIxx : idempotent gcdGI.
+Lemma gcdGIxx : idempotent_op gcdGI.
 Proof. by move=> x; rewrite gcdGIE ltnn modGIxx gcd0GI. Qed.
 
 Lemma dvdGI_mod d x y : d %| x -> (d %| y) = (d %| y %% x).

meta.yml

@@ -49,29 +49,29 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.18 or later'
-  opam: '{(>= "8.18")}'
+  text: '8.20 or later'
+  opam: '{(>= "8.20")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.3.0")}'
   description: |-
-    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.3 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.3.0")}'
   description: |-
-    [MathComp algebra 2.1 or later](https://math-comp.github.io)
+    [MathComp algebra 2.3 or later](https://math-comp.github.io)
 
 - opam:
     name: coq-mathcomp-field
-    version: '{(>= "2.1.0")}'
+    version: '{(>= "2.3.0")}'
   description: |-
-    [MathComp field 2.1 or later](https://math-comp.github.io)
+    [MathComp field 2.3 or later](https://math-comp.github.io)
 
 tested_coq_opam_versions:
-- version: '2.1.0-coq-8.18'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 
 namespace: twoSquare