Skip to content

Cleanup old compat code #122

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Mar 24, 2026
Merged

Cleanup old compat code #122

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/mpoly.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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)
Expand Down
11 changes: 0 additions & 11 deletions src/ssrcomplements.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,17 +16,6 @@

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))
Expand Down Expand Up @@ -181,7 +170,7 @@
Lemma in_allpairs (S T R : eqType) (f : S -> T -> R)
(s : seq S) (t : seq T) x y :
injective (uncurry f) ->
f x y \in [seq f x0 y0 | x0 <- s, y0 <- t] =

Check warning on line 173 in src/ssrcomplements.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

In term, tolerating this expression at a higher level than expected
(x \in s) && (y \in t).
Proof.
move=> f_inj; apply/allpairsP/andP => [|[]]; last by exists (x, y).
Expand Down
Loading