Handle a few deprecation warnings (#78)

coq-community · Apr 22, 2023 · 4aa6e03 · 4aa6e03
1 parent 1063846
commit 4aa6e03
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 8 deletions.
diff --git a/refinements/binnat.v b/refinements/binnat.v
@@ -373,7 +373,7 @@ Qed.
 Lemma Rnat_ltE (c d : N) : (c < d)%C = (spec_N c < spec_N d).
 Proof.
 symmetry; eapply refines_eq.
-change (spec_N c < spec_N d) with (rel_of_simpl_rel ltn (spec_N c) (spec_N d)).
+change (spec_N c < spec_N d) with (rel_of_simpl ltn (spec_N c) (spec_N d)).
 refines_apply1; first refines_apply1.
 refines_abstr.
 Qed.

diff --git a/refinements/binord.v b/refinements/binord.v
@@ -156,7 +156,7 @@ Local Opaque ltn.
           (fun x y => ltn x y) lt_op.
 Proof.
   rewrite refinesE=> x x' hx y y' hy /=.
-  try change (pred_of_simpl (ltn x) y) with (rel_of_simpl_rel ltn x y).
+  try change (pred_of_simpl (ltn x) y) with (rel_of_simpl ltn x y).
   exact: refinesP.
 Qed.
 
@@ -180,4 +180,4 @@ Qed.
   refines (Rord rn ==> Rnat) (@nat_of_ord n1) id.
 Proof. by rewrite refinesE. Qed.
 
-End binord_theory.
+End binord_theory.
diff --git a/refinements/binrat.v b/refinements/binrat.v
@@ -216,14 +216,13 @@ Lemma Z2int_div x y : Z.le 0 x -> Z.le 0 y ->
 Proof.
 case: x => [|x|//] _; [by rewrite intdiv.div0z|].
 case: y => [|y|//] _; [by rewrite intdiv.divz0|].
-rewrite -!positive_nat_Z -div_Zdiv; last first.
-{ rewrite Nat.neq_0_lt_0; exact: Pos2Nat.is_pos. }
+rewrite -!positive_nat_Z -Nat2Z.inj_div; last first.
 rewrite !positive_nat_Z /= /divz gtr0_sgz ?mul1r; last first.
 { exact: nat_of_pos_gt0. }
 rewrite divE !binnat.to_natE absz_nat /Z2int.
 move: (Zle_0_nat (nat_of_pos x %/ nat_of_pos y)).
 rewrite -[X in _ = Posz X]Nat2Z.id.
-  by case: Z.of_nat => //= p _; rewrite binnat.to_natE.
+by case: Z.of_nat => //= p _; rewrite binnat.to_natE.
 Qed.
 
 Lemma Z2int_le x y : (Z2int x <= Z2int y)%R <-> Z.le x y.

diff --git a/theory/edr.v b/theory/edr.v
@@ -321,7 +321,7 @@ have Hfg2 : {subset codom f2 <= codom g2}.
   move=> x /codomP [y ->].
   rewrite codomE /f2 /g2 -Hfg0 map_comp (mem_map Hg).
   have: p (lift p0 y) \in enum 'I_j.+1 by rewrite mem_enum.
-  rewrite enum_ordS in_cons -(permKV p ord0).
+  rewrite enum_ordSl in_cons -(permKV p ord0).
   by rewrite (inj_eq (@perm_inj _ _)) eq_sym (negbTE (neq_lift _ _)).
 rewrite addr0 (bigD1 ((p^-1)%g ord0)) //= -Hfg0 permKV eqxx eqd_mull //.
 rewrite -[X in _ %= X]mul1r eqd_mul ?eqd1 ?unitrX ?unitrN ?unitr1 //.

diff --git a/theory/smith_complements.v b/theory/smith_complements.v
@@ -168,7 +168,7 @@ rewrite (expand_det_row _ ((p^-1)%g ord0)) big_ord_recl big1=>[|i _].
     rewrite codomE /f2 /g2 -Hfg0 map_comp (mem_map Hg).
     set i := p _.
     have:= mem_ord_enum i.
-    rewrite -enum_ord_enum enum_ordS in_cons -(permKV p ord0).
+    rewrite -enum_ord_enum enum_ordSl in_cons -(permKV p ord0).
     by rewrite /i (inj_eq (@perm_inj _ _)) eq_sym (negbTE (neq_lift _ _)).
   rewrite addr0 (bigD1 ((p^-1)%g ord0)) //= -Hfg0 permKV eqxx eqd_mull //.
   rewrite -[X in _ %= X]mul1r eqd_mul ?eqd1 ?unitrX ?unitrN ?unitr1 //.