From 28719778771b1e17ef317a7053a299d1ec42f6e8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 28 Jun 2024 16:12:23 +0200 Subject: [PATCH 1/2] [CI] Update --- .github/workflows/docker-action.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 5cc922d..9e1821f 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -25,8 +25,6 @@ jobs: - 'mathcomp/mathcomp:2.2.0-coq-8.18' - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.2.0-coq-dev' - - 'mathcomp/mathcomp-dev:coq-8.16' - - 'mathcomp/mathcomp-dev:coq-8.17' - 'mathcomp/mathcomp-dev:coq-8.18' - 'mathcomp/mathcomp-dev:coq-8.19' - 'mathcomp/mathcomp-dev:coq-dev' From 1d8c3fc1fb0e964a30874f6aa4007813f1f5ee52 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 28 Jun 2024 16:11:40 +0200 Subject: [PATCH 2/2] Adapt to https://github.com/math-comp/math-comp/pull/1223 --- theory/polydvd.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theory/polydvd.v b/theory/polydvd.v index 07cf6b2..03031a7 100644 --- a/theory/polydvd.v +++ b/theory/polydvd.v @@ -97,7 +97,7 @@ move: (erefl om); rewrite /om /d; case: {2}_ / ihn. by rewrite add1n (leq_trans spq) // leqnSn. rewrite size_proper_mul ?lead_coefC ?lead_coefXn ?mulr1 //. rewrite size_polyC x0 size_polyXn /= addnS /=. - by rewrite addnBA // leq_subLR leq_add2r size_poly. + by rewrite ?add0n ?addnS addnBA//= leq_subLR leq_add2r size_poly. * move=> s hs; case hpq: (odivp_rec _ _ _ _)=> [r'|] //=. case=> hm; constructor; move: hm; rewrite opprD addrA. move/eqP; rewrite (can2_eq (@addrNK _ _) (@addrK _ _)) => /eqP->. @@ -769,7 +769,7 @@ case: {1}_ / h=> //. by rewrite add1n (leq_trans spq) // leqnSn. rewrite size_proper_mul ?lead_coefC ?lead_coefXn ?mulr1 ?x0 //. rewrite size_polyC x0 size_polyXn /= addnS /=. - by rewrite addnBA // leq_subLR leq_add2r size_poly. + by rewrite ?add0n ?addnS addnBA//= leq_subLR leq_add2r size_poly. move=> q1 r0 H G. move/eqP; rewrite xpair_eqE; case/andP; move/eqP=> q1q0; move/eqP=> r0r. constructor; last by rewrite -r0r.