diff --git a/.circleci/config.yml b/.circleci/config.yml
index 2c62d13..66a831a 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -101,6 +101,17 @@ jobs:
     - image: coqorg/coq:8.19
     resource_class: 'large'
 
+  coq-8-19-mathcomp-2-3-0:
+    <<: *defaults
+    steps:
+    - startup
+    - prepare:
+        mathcomp-version: '2.3.0'
+    - build
+    docker:
+    - image: coqorg/coq:8.19
+    resource_class: 'large'
+
   coq-8-19-mathcomp-dev:
     <<: *defaults
     steps:
@@ -131,5 +142,6 @@ workflows:
     - coq-8-18-mathcomp-2-0-0
     - coq-8-18-mathcomp-dev
     - coq-8-19-mathcomp-2-2-0
+    - coq-8-19-mathcomp-2-3-0
     - coq-8-19-mathcomp-dev
     - coq-dev
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3326f75..67922a2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,15 +10,21 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Changed
 
-- Use new display type for `orderType`, as in MathComp 2.3.0.  The generated
-  instances now use the default display.
-
 ### Deprecated
 
 ### Removed
 
 ### Fixed
 
+## [0.2.1] - 2024-12-02
+
+### Changed
+
+- Use new display type for `orderType`, as in MathComp 2.3.0.  The generated
+  instances now use the default display.
+
+### Fixed
+
 - Simplify the type of derived isFinite instances to avoid a non-forgetful
   inheritance warning.
 
@@ -48,7 +54,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 - First version supporting inductive types.
 
-[Unreleased]: https://github.com/arthuraa/deriving/compare/v0.2.0...HEAD
+[Unreleased]: https://github.com/arthuraa/deriving/compare/v0.2.1...HEAD
+[0.2.1]: https://github.com/arthuraa/deriving/releases/tag/v0.2.1
 [0.2.0]: https://github.com/arthuraa/deriving/releases/tag/v0.2.0
 [0.1.1]: https://github.com/arthuraa/deriving/releases/tag/v0.1.1
 [0.1.0]: https://github.com/arthuraa/deriving/releases/tag/v0.1.0
diff --git a/CoqMakefile.local b/CoqMakefile.local
index e2cbf2d..269f48c 100644
--- a/CoqMakefile.local
+++ b/CoqMakefile.local
@@ -3,7 +3,7 @@ TESTVOFILES=$(TESTVFILES:.v=.vo)
 UNFOLDFILES = theories/ind.v theories/base.v
 
 theories/tactics.v: make_tactics.ml $(UNFOLDFILES)
-	ocaml str.cma make_tactics.ml $(UNFOLDFILES) > theories/tactics.v
+	ocaml -I +str str.cma make_tactics.ml $(UNFOLDFILES) > theories/tactics.v
 
 test: $(TESTVOFILES)
 .PHONY: test
diff --git a/README.md b/README.md
index 063f94b..b869891 100644
--- a/README.md
+++ b/README.md
@@ -81,9 +81,9 @@ In such cases, it is a good idea to keep the instance opaque (e.g. defined with
 
 ## Requirements
 
-- Coq 8.17 -- 8.18
+- Coq 8.17 -- 8.19
 
-- `coq-mathcomp-ssreflect` 2.0.0
+- `coq-mathcomp-ssreflect` 2.0.0 -- 2.3.0
 
 ## Installation
 
diff --git a/_CoqProject b/_CoqProject
index ce35a4d..c6e8ee3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,6 +11,7 @@ theories/ind.v
 theories/tactics.v
 theories/infer.v
 theories/instances.v
+theories/compat.v
 theories/deriving.v
 
 theories/instances/eqtype.v
diff --git a/flake.lock b/flake.lock
index fa58f12..6f22028 100644
--- a/flake.lock
+++ b/flake.lock
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1694948089,
-        "narHash": "sha256-d2B282GmQ9o8klc22/Rbbbj6r99EnELQpOQjWMyv0rU=",
+        "lastModified": 1733064805,
+        "narHash": "sha256-7NbtSLfZO0q7MXPl5hzA0sbVJt6pWxxtGWbaVUDDmjs=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "5148520bfab61f99fd25fb9ff7bfbb50dad3c9db",
+        "rev": "31d66ae40417bb13765b0ad75dd200400e98de84",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index ee37b4f..c69c0dd 100644
--- a/flake.nix
+++ b/flake.nix
@@ -12,13 +12,13 @@
     flake-utils.lib.eachDefaultSystem (system:
       let pkgs = nixpkgs.legacyPackages.${system}; in rec {
             packages = rec {
-              coq = pkgs.coq_8_17;
-              coqPackages = pkgs.coqPackages_8_17.overrideScope' (self: super:
+              coq = pkgs.coq_8_19;
+              coqPackages = pkgs.coqPackages_8_19.overrideScope (self: super:
                 { mathcomp = super.mathcomp.override {
-                    version = "2.0.0";
+                    version = "2.2.0";
                   };
                   deriving = super.deriving.overrideAttrs {
-                    version = "0.2.0";
+                    version = "0.2.1";
                     src = ./.;
                   };
                 });
diff --git a/tests/syntax.v b/tests/syntax.v
index 0a4c30c..3848a9a 100644
--- a/tests/syntax.v
+++ b/tests/syntax.v
@@ -154,9 +154,9 @@ HB.instance Definition _ := expr_isCountable.
 Definition val_isCountable :=
   [derive isCountable for val].
 HB.instance Definition _ := val_isCountable.
-Definition expr_isOrder : Order.isOrder tt expr.
+Definition expr_isOrder : Order.isOrder Order.default_display expr.
 Proof. exact: [derive nored isOrder for expr]. Qed.
 HB.instance Definition _ := expr_isOrder.
-Definition val_isOrder : Order.isOrder tt val.
+Definition val_isOrder : Order.isOrder Order.default_display val.
 Proof. exact: [derive nored isOrder for val]. Qed.
 HB.instance Definition _ := val_isOrder.
diff --git a/theories/base.v b/theories/base.v
index 9a24972..4736287 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1308,13 +1308,3 @@ Definition hnth1 m :=
 Coercion hnth1 : hlist1 >-> Funclass.
 #[global]
 Hint Unfold hnth1 : deriving.
-
-(* Compatibility layer for Order.disp_t introduced in MathComp 2.3            *)
-(* TODO: remove when we drop the support for MathComp 2.2                     *)
-Module Order.
-Import Order.
-Definition disp_t : Set.
-Proof. exact: disp_t || exact: unit. Defined.
-Definition default_display : disp_t.
-Proof. exact: tt || exact: Disp tt tt. Defined.
-End Order.
diff --git a/theories/compat.v b/theories/compat.v
new file mode 100644
index 0000000..c36b32d
--- /dev/null
+++ b/theories/compat.v
@@ -0,0 +1,18 @@
+From HB Require Import structures.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Set Primitive Projections.
+
+(* Compatibility layer for Order.disp_t introduced in MathComp 2.3            *)
+(* TODO: remove when we drop the support for MathComp 2.2                     *)
+Module Order.
+Import Order.
+Definition disp_t : Set.
+Proof. exact: disp_t || exact: unit. Defined.
+Definition default_display : disp_t.
+Proof. exact: tt || exact: Disp tt tt. Defined.
+End Order.
diff --git a/theories/deriving.v b/theories/deriving.v
index 568d764..99e6a43 100644
--- a/theories/deriving.v
+++ b/theories/deriving.v
@@ -1 +1 @@
-From deriving Require Export ind tactics infer instances.
+From deriving Require Export ind tactics infer instances compat.
diff --git a/theories/instances.v b/theories/instances.v
index 892edd1..ef99ca5 100644
--- a/theories/instances.v
+++ b/theories/instances.v
@@ -2,7 +2,7 @@ From HB Require Import structures.
 From mathcomp Require Import
   ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
 
-From deriving Require Import base ind tactics infer.
+From deriving Require Import base ind tactics infer compat.
 From deriving.instances Require Export eqtype tree_of_ind fintype order.
 
 From Coq Require Import ZArith NArith String Ascii.
diff --git a/theories/instances/order.v b/theories/instances/order.v
index 250dd30..2994354 100644
--- a/theories/instances/order.v
+++ b/theories/instances/order.v
@@ -1,7 +1,7 @@
 From mathcomp Require Import
   ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype order.
 
-From deriving Require Import base ind tactics infer.
+From deriving Require Import base ind tactics infer compat.
 
 From Coq Require Import ZArith NArith String Ascii.