Merge pull request #93 from math-comp/ci

Update CI

.github/workflows/docker-action.yml

@@ -20,6 +20,10 @@ jobs:
           - '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.0.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.16'
           - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'
@@ -40,6 +44,7 @@ jobs:
         if: ${{ always() }}
         run: sudo chown -R 1001:116 .
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -16,7 +16,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
 the Mathematical Components library. These tactics use the algebraic
 structures defined in the MathComp library and their canonical instances for
 the instance resolution, and do not require any special instance declaration,
-like the `add Ring` and `Add Field` commands. Therefore, each of these tactics
+like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics
 works with any instance of the respective structure, including concrete
 instances declared through Hierarchy Builder, abstract instances, and mixed
 concrete and abstract instances, e.g., `int * R` where `R` is an abstract

coq-mathcomp-algebra-tactics.opam

@@ -16,7 +16,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
 the Mathematical Components library. These tactics use the algebraic
 structures defined in the MathComp library and their canonical instances for
 the instance resolution, and do not require any special instance declaration,
-like the `add Ring` and `Add Field` commands. Therefore, each of these tactics
+like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics
 works with any instance of the respective structure, including concrete
 instances declared through Hierarchy Builder, abstract instances, and mixed
 concrete and abstract instances, e.g., `int * R` where `R` is an abstract

meta.yml

@@ -13,7 +13,7 @@ description: |-
   the Mathematical Components library. These tactics use the algebraic
   structures defined in the MathComp library and their canonical instances for
   the instance resolution, and do not require any special instance declaration,
-  like the `add Ring` and `Add Field` commands. Therefore, each of these tactics
+  like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics
   works with any instance of the respective structure, including concrete
   instances declared through Hierarchy Builder, abstract instances, and mixed
   concrete and abstract instances, e.g., `int * R` where `R` is an abstract
@@ -52,6 +52,14 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.17'