From e7cbfb5369f55d91c0dd23227785b280bb2602bd Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 24 Mar 2026 08:39:25 +0100
Subject: [PATCH] Cleanup old compat code

---
 src/mpoly.v          |  6 +++---
 src/ssrcomplements.v | 11 -----------
 2 files changed, 3 insertions(+), 14 deletions(-)

diff --git a/src/mpoly.v b/src/mpoly.v
index b514e39..03a6475 100644
--- a/src/mpoly.v
+++ b/src/mpoly.v
@@ -503,7 +503,7 @@ apply/esym; rewrite andbC /mnmc_lt /mnmc_le lt_def lexi_cons eqseq_cons.
 by case: ltgtP; rewrite //= 1?andbC //; apply/contra_ltN => /eqP ->.
 Qed.
 
-HB.instance Definition _ := Order.isPOrder.Build Order.default_display 'X_{1..n}
+HB.instance Definition _ := Order.isPOrder.Build (Order.Disp tt tt) 'X_{1..n}
   ltmc_def lemc_refl lemc_anti lemc_trans.
 
 Lemma leEmnm m1 m2 : (m1 <= m2)%O = (mdeg m1 :: val m1 <= mdeg m2 :: val m2)%O.
@@ -513,7 +513,7 @@ Lemma ltEmnm m m' : (m < m')%O = (mdeg m :: m < mdeg m' :: m')%O.
 Proof. by []. Qed.
 
 HB.instance Definition _ :=
-  Order.POrder_isTotal.Build Order.default_display 'X_{1..n} lemc_total.
+  Order.POrder_isTotal.Build (Order.Disp tt tt) 'X_{1..n} lemc_total.
 
 Lemma le0m m : (0%MM <= m)%O.
 Proof.
@@ -523,7 +523,7 @@ by rewrite -lt0n mdeg0 lexi_cons leEnat; case: ltngtP.
 Qed.
 
 HB.instance Definition _ :=
-  Order.hasBottom.Build Order.default_display 'X_{1..n} le0m.
+  Order.hasBottom.Build (Order.Disp tt tt) 'X_{1..n} le0m.
 
 Lemma ltmcP m1 m2 : mdeg m1 = mdeg m2 -> reflect
   (exists2 i : 'I_n, forall (j : 'I_n), j < i -> m1 j = m2 j & m1 i < m2 i)
diff --git a/src/ssrcomplements.v b/src/ssrcomplements.v
index 6401c20..d346cb1 100644
--- a/src/ssrcomplements.v
+++ b/src/ssrcomplements.v
@@ -16,17 +16,6 @@ Unset Printing Implicit Defensive.
 
 Import Order.Theory GRing.Theory.
 
-(* -------------------------------------------------------------------- *)
-(* 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.
-
 (* -------------------------------------------------------------------- *)
 Lemma lreg_prod (T : eqType) (R : pzRingType) (r : seq T) (P : pred T) (F : T -> R):
       (forall x, x \in r -> P x -> GRing.lreg (F x))