diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 03aa660..5cc922d 100644
--- a/.github/workflows/docker-action.yml
+++ b/.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'
diff --git a/README.md b/README.md
index c7b71dc..c413585 100644
--- a/README.md
+++ b/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`
diff --git a/coq-coqeal.opam b/coq-coqeal.opam
index b9c99dd..2ede11a 100644
--- a/coq-coqeal.opam
+++ b/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"}
diff --git a/meta.yml b/meta.yml
index 345761c..520ff9c 100644
--- a/meta.yml
+++ b/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'
diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v
index 576dd9d..4726e79 100644
--- a/refinements/examples/irred.v
+++ b/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 :=