Merge pull request #89 from coq-community/mc_1190

Drop MC 2.0 support

.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'

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`

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"}

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'

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