Adapt to math-comp/math-comp#1166

src/mpoly.v

@@ -247,7 +247,7 @@
 Definition mnm1 (c : 'I_n) := [multinom c == i | i < n].
 Definition mnm_add m1 m2 := [multinom m1 i + m2 i | i < n].
 Definition mnm_sub m1 m2 := [multinom m1 i - m2 i | i < n].
 Definition mnm_muln m i := nosimpl iterop _ i mnm_add m mnm0.
 
 Local Notation "0"         := mnm0 : multi_scope.
 Local Notation "'U_(' n )" := (mnm1 n) : multi_scope.
@@ -519,7 +519,7 @@
 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 @@
 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 @@
 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)
@@ -793,7 +795,7 @@
 Lemma mpolyCK : cancel mpolyC (mcoeff 0%MM).
 Proof. by move=> c; rewrite mcoeffC eqxx mulr1. Qed.
 
 Definition msupp p : seq 'X_{1..n} := nosimpl (dom p).
 
 Lemma msuppE p : msupp p = dom p :> seq _.
 Proof. by []. Qed.
@@ -1623,7 +1625,7 @@
 Canonical mpolyX_unlockable m := [unlockable of (mpolyX m)].
 
 Definition mX (k : 'I_n) : 'X_{1..n} :=
   nosimpl [multinom (i == k : nat) | i < n].
 
 End MPolyVar.
 
@@ -3729,10 +3731,10 @@
 Proof.
 rewrite -sum1dep_card -(big_ord_widen _ (fun _ => 1%N)) //=.
 by rewrite sum1_card card_ord.
 Qed.
 
 Let mesymlmE k : mesymlm k = [multinom (i < k : nat) | i < n].
 Proof. by apply/mnmP=> i; rewrite !mnmE in_set. Qed.
 
 Let mesymlm_max (h : {set 'I_n}) : #|h| <= n -> (mesym1 h <= mesymlm #|h|)%O.
 Proof.                        (* FIXME: far too convoluted *)
@@ -3762,7 +3764,7 @@
   by case: (boolP (j \in h))=> // /i0_min; rewrite leqNgt lt_j_i0.
 + move=> i0 i0_notin_h i0_min; rewrite !mnmE in_set.
   by rewrite (negbTE i0_notin_h) lt0n // (@leq_ltn_trans i) // i0_min.
 Qed.
 
 Lemma mesym_neq0 k (le_kn : k <= n) : 's_k != 0 :> {mpoly R[n]}.
 Proof.
@@ -4013,7 +4015,7 @@
   end.
 
 Definition muni (p : {mpoly R[n.+1]}) : {poly {mpoly R[n]}} :=
   nosimpl (mmap (polyC \o @mpolyC _ _) X p).
 
 Let XE m : mmap1 X m = 'X_[[multinom (m (widen i)) | i < n]] *: 'X^(m ord_max).
 Proof.
@@ -4027,7 +4029,7 @@
 rewrite /mmap1 big_ord_recr /= X1 -mul_polyC.
 rewrite mpolyXE_id rmorph_prod /=; congr (_ * _).
 by apply/eq_bigr=> i _; rewrite X2 rmorphXn /= mnmE.
 Qed.
 
 Lemma muniE p : muni p =
   \sum_(m <- msupp p)
@@ -4102,7 +4104,7 @@
   (only parsing).
 
 Let inj_widen n : injective (widen : 'I_n -> _).
 Proof. by move=> x y /eqP; rewrite eqE /= val_eqE => /eqP. Qed.
 
 Local Hint Resolve inj_widen : core.
 
@@ -4113,7 +4115,7 @@
   by move=> x_in_m; exists x.
 move=> m1 m2 /= /setP eq; apply/setP=> /= x.
 by have := eq (widen x); rewrite !h.
 Qed.
 
 Local Hint Resolve inj_swiden : core.
 
@@ -4126,7 +4128,7 @@
   apply/negP; case/imsetP=> /= y _ /eqP.
   by rewrite eqE /= eq_sym ltn_eqF.
 by rewrite !E.
 Qed.
 
 Let disjoint_S n k : [disjoint (S1 n k) & (S2 n k)].
 Proof.
@@ -4136,7 +4138,7 @@
 move/setP/(_ ord_max); rewrite in_set in_set1 eqxx /=.
 case/imsetP=> /= {h1 h2} m _ /eqP.
 by rewrite eqE /= eq_sym ltn_eqF.
 Qed.
 
 Let union_S n k :
   [set h in {set 'I_n.+1} | #|h| == k.+1] = S1 n k :|: S2 n k.
@@ -4155,7 +4157,7 @@
   try exact/inj_swiden; try exact/inj_mDswiden.
   (* remove the line above once requiring Coq >= 8.17 *)
 by rewrite !card_ord binS.
 Qed.
 
 Lemma mesymSS (R : ringType) n k :
   's_(n.+1, k.+1) = mw 's_(n, k.+1) + mw 's_(n, k) * 'X_(ord_max)
@@ -4282,7 +4284,7 @@
 apply/mnmP=> i; apply/esym; rewrite mnm_sumE mnmE big_mkcond /=.
 apply/eq_bigr=> j _; rewrite mnmE; case: leqP=> _.
   by rewrite mul1n. by rewrite mul0n.
 Qed.
 
 Let mleadc_XS l : mleadc ('X_[l] \mPo S) = 1.
 Proof.
@@ -4436,7 +4438,7 @@
 Qed.
 
 Definition symf (p : {mpoly R[n]}) :=
   nosimpl (symfn (tag (symfnS p)) p).1.
 
 Lemma symfP (p : {mpoly R[n]}) : p \is symmetric -> p = symf p \mPo S.
 Proof.
@@ -4918,7 +4920,7 @@
 (* -------------------------------------------------------------------- *)
 Context (n : nat) (R : ringType) (d : nat).
 
 Lemma dhomog_vecaxiom: vector_axiom 'C(d + n, d) (dhomog n.+1 R d).
 Proof.
 pose b := sbasis n.+1 d.
 pose t := [tuple of nseq d (0 : 'I_n.+1)].

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)