Adapt to math-comp/math-comp#1166

math-comp · Mar 15, 2024 · fdc4929 · fdc4929
1 parent 07713f4
commit fdc4929
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 5 deletions.
diff --git a/src/mpoly.v b/src/mpoly.v
@@ -519,7 +519,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 tt 'X_{1..n}
+HB.instance Definition _ := Order.isPOrder.Build Order.default_display '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.
@@ -528,7 +528,8 @@ Proof. by []. Qed.
 Lemma ltEmnm m m' : (m < m')%O = (mdeg m :: m < mdeg m' :: m')%O.
 Proof. by []. Qed.
 
-HB.instance Definition _ := Order.POrder_isTotal.Build tt 'X_{1..n} lemc_total.
+HB.instance Definition _ :=
+  Order.POrder_isTotal.Build Order.default_display 'X_{1..n} lemc_total.
 
 Lemma le0m m : (0%MM <= m)%O.
 Proof.
@@ -537,7 +538,8 @@ rewrite leEmnm; have [/eqP|] := eqVneq (mdeg m) 0%N.
 by rewrite -lt0n mdeg0 lexi_cons leEnat; case: ltngtP.
 Qed.
 
-HB.instance Definition _ := Order.hasBottom.Build tt 'X_{1..n} le0m.
+HB.instance Definition _ :=
+  Order.hasBottom.Build Order.default_display '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
@@ -15,6 +15,17 @@ 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 : ringType) (r : seq T) (P : pred T) (F : T -> R):
       (forall x, x \in r -> P x -> GRing.lreg (F x))
@@ -235,7 +246,7 @@ Qed.
 
 (* -------------------------------------------------------------------- *)
 Section LatticeMisc.
-Context {T : eqType} {disp : unit} {U : bDistrLatticeType disp}.
+Context {T : eqType} {disp : Order.disp_t} {U : bDistrLatticeType disp}.
 Context (P : pred T) (F : T -> U).
 
 Implicit Type (r : seq T).
@@ -275,7 +286,7 @@ End LatticeMisc.
 
 (* -------------------------------------------------------------------- *)
 Section WF.
-Context {disp : unit} {T : porderType disp}.
+Context {disp : Order.disp_t} {T : porderType disp}.
 
 Hypothesis wf: forall (P : T -> Type),
      (forall x, (forall y, y < x -> P y) -> P x)