Skip to content

Commit

Permalink
Fix deprecation warnings from MathComp 1.17.0
Browse files Browse the repository at this point in the history
  • Loading branch information
@proux01
proux01 committed Jun 7, 2023
1 parent 529bc16 commit 132fd79
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 12 deletions.
6 changes: 3 additions & 3 deletions theories/common.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ apply: mk_SOR_theory.
+ by left.
+ by right; right.
+ by right; left.
- by move=> x y z; rewrite ler_add2l.
- by move=> x y z; rewrite lerD2l.
- exact: mulr_gt0.
- by apply/eqP; rewrite eq_sym oner_neq0.
Qed.
Expand Down Expand Up @@ -340,8 +340,8 @@ Qed.
Lemma R_of_Q_le x y : Qle_bool x y = (R_of_Q x <= R_of_Q y :> F).
Proof.
rewrite /Qle_bool /R_of_Q /=.
rewrite ler_pdivr_mulr ?ltr0n; last lia.
rewrite mulrAC ler_pdivl_mulr ?ltr0n; last lia.
rewrite ler_pdivrMr ?ltr0n; last lia.
rewrite mulrAC ler_pdivlMr ?ltr0n; last lia.
rewrite !pmulrn -!intrM ler_int; lia.
Qed.

Expand Down
4 changes: 2 additions & 2 deletions theories/lra.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ move: f; elim: e => {R} //=.
- by move=> R e1 IHe1 e2 IHe2 f; rewrite mulE rmorphMz -mulrzr IHe1 IHe2.
- by move=> R f; rewrite R_of_ZE rmorph1.
- by move=> R e1 IHe1 e2 IHe2 f; rewrite mulE rmorphM IHe1 IHe2.
- by move=> R e IHe n f; rewrite expE rmorphX IHe large_nat_N_nat.
- by move=> R e IHe n f; rewrite expE rmorphXn IHe large_nat_N_nat.
- by move=> R S g e IHe f; rewrite -IHe.
- by move=> x f; rewrite R_of_ZE -(rmorph_int f) intz large_int_Z_int.
- by move=> x f; rewrite R_of_ZE -(rmorph_int f); congr (f _); lia.
Expand Down Expand Up @@ -297,7 +297,7 @@ move: f; elim: e => {R} //=.
move: (IHe1 f) (IHe2 f) => [{}IHe1 IHe1'] [{}IHe2 IHe2'].
by rewrite mulE rmorphM invfM IHe1' IHe1 IHe2' IHe2.
- move=> R e IHe n f; case: (IHe f) => {}IHe IHe'.
by rewrite expE rmorphX -exprVn IHe' IHe large_nat_N_nat.
by rewrite expE rmorphXn -exprVn IHe' IHe large_nat_N_nat.
- move=> R e IHe f; case: (IHe f) => {}IHe IHe'.
by rewrite fmorphV invrK IHe' IHe.
- by move=> R S g e IHe f; case: (IHe (f \o g)); split.
Expand Down
14 changes: 7 additions & 7 deletions theories/ring.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,10 +227,10 @@ move: f; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=.
- by move=> R f; rewrite rmorph1 oneE.
- by move=> R e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2 mulE.
- by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2 mulE.
- by move=> R e1 IHe1 e2 f; rewrite rmorphX IHe1 expE large_nat_N_nat.
- by move=> R e1 IHe1 e2 f; rewrite rmorphX IHe1 expE large_nat_N_nat.
- by move=> R e1 IHe1 e2 f; rewrite rmorphXn IHe1 expE large_nat_N_nat.
- by move=> R e1 IHe1 e2 f; rewrite rmorphXn IHe1 expE large_nat_N_nat.
- move=> e1 IHe1 [|n|n] f; rewrite !(zeroE, expE, rmorph0, rmorph1) //=.
rewrite -IHe1 -rmorphX; congr (f _); lia.
rewrite -IHe1 -rmorphXn; congr (f _); lia.
- by move=> R S g e1 IHe1 f; rewrite -IHe1.
- by move=> V R g e1 IHe1 f; rewrite -IHe1.
- by move=> e f; rewrite -[Posz _]intz rmorph_int [LHS]Nnorm_correct.
Expand Down Expand Up @@ -323,12 +323,12 @@ move: f; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=.
- by move=> R f; rewrite rmorph1 oneE.
- by move=> R e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2 mulE.
- by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2 mulE.
- by move=> R e1 IHe1 e2 f; rewrite rmorphX IHe1 expE large_nat_N_nat.
- by move=> R e1 IHe1 n f; rewrite rmorphX IHe1 expE large_nat_N_nat.
- move=> R e1 IHe1 n f; rewrite fmorphV rmorphX IHe1 invE expE.
- by move=> R e1 IHe1 e2 f; rewrite rmorphXn IHe1 expE large_nat_N_nat.
- by move=> R e1 IHe1 n f; rewrite rmorphXn IHe1 expE large_nat_N_nat.
- move=> R e1 IHe1 n f; rewrite fmorphV rmorphXn IHe1 invE expE.
by rewrite Nnat.N2Nat.inj_succ large_nat_N_nat.
- move=> e1 IHe1 [|n|n] f; rewrite ?(zeroE, oneE, expE, rmorph0, rmorph1) //=.
rewrite -IHe1 -rmorphX; congr (f _); lia.
rewrite -IHe1 -rmorphXn; congr (f _); lia.
- by move=> F' e1 IHe1 f; rewrite fmorphV IHe1 invE.
- by move=> R R' g e1 IHe1 f; rewrite -IHe1.
- by move=> V R g e1 IHe1 f; rewrite -IHe1.
Expand Down

0 comments on commit 132fd79

Please sign in to comment.