diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index e6d55d8..ed173c2 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -29,6 +29,10 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.20'
diff --git a/Make b/Make
index e6f5a68..de7cafd 100644
--- a/Make
+++ b/Make
@@ -5,3 +5,4 @@ theories/ring.v
 -R theories mathcomp.algebra_tactics
 -arg -w -arg -notation-overridden
 -arg -w -arg +elpi.typecheck
+-arg -w -arg -elpi.typecheck-syntax
diff --git a/_CoqProject b/_CoqProject
index 89f1677..7dc6b05 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,3 +1,4 @@
 -R theories mathcomp.algebra_tactics
 -arg -w -arg -notation-overridden
 -arg -w -arg +elpi.typecheck
+-arg -w -arg -elpi.typecheck-syntax
diff --git a/meta.yml b/meta.yml
index 1254e4a..a6d18ea 100644
--- a/meta.yml
+++ b/meta.yml
@@ -70,6 +70,14 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
@@ -203,7 +211,7 @@ documentation: |-
   constant is automatically resolved.
 
   The `field` tactic has a preprocessor similar to the `ring` tactic.
-  In addition ot the constructs supported by the `ring` tactic, the `field`
+  In addition to the constructs supported by the `ring` tactic, the `field`
   tactic supports `GRing.inv` and `exprz` with a negative exponent.
 
   ### The `lra`, `nra`, and `psatz` tactics