Remove a few warnings

Among them deprecation warning that canbe followed since we only support Mathcomp 1.10.
coq-community · Feb 3, 2020 · 1be58ee · 1be58ee
1 parent 521cd90
commit 1be58ee
Show file tree

Hide file tree

Showing 11 changed files with 26 additions and 28 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -19,7 +19,7 @@ env:
   - COQ_IMAGE="mathcomp/mathcomp:1.10.0-coq-8.9"
   - COQ_IMAGE="mathcomp/mathcomp:1.10.0-coq-8.10"
   - COQ_IMAGE="mathcomp/mathcomp:1.10.0-coq-8.11"
-  - COQ_IMAGE="mathcomp/mathcomp:1.9.0-coq-dev"
+  #- COQ_IMAGE="mathcomp/mathcomp:1.10.0-coq-dev"
   #- COQ_IMAGE="mathcomp/mathcomp-dev:coq-8.7"
   #- COQ_IMAGE="mathcomp/mathcomp-dev:coq-8.8"
   #- COQ_IMAGE="mathcomp/mathcomp-dev:coq-8.9"

diff --git a/refinements/binint.v b/refinements/binint.v
@@ -463,10 +463,10 @@ End binint_nat_pos.
 End binint_parametricity.
 End binint_theory.
 
-Section testint.
-
 From CoqEAL Require Import binnat.
 
+Section testint.
+
 Goal (0 == 0 :> int).
 by coqeal.
 Abort.
@@ -499,4 +499,4 @@ Goal (1000%:Z == 2%:Z * 500%:Z).
 by coqeal.
 Abort.
 
-End testint.
+End testint.
diff --git a/refinements/examples/irred.v b/refinements/examples/irred.v
@@ -197,7 +197,7 @@ Lemma card'_perm (T : eqType) (s s' : seq T) (P : pred T) :
   perm_eq s s' -> card' s P = card' s' P :> nat.
 Proof.
 move=> peq_ss'; rewrite /card' /size_op !size_seqE.
-by apply/perm_eq_size/perm_eqP=> x; rewrite !count_filter; apply/perm_eqP.
+by apply/perm_size/seq.permP=> x; rewrite !count_filter; apply/seq.permP.
 Qed.
 
 Lemma card'E (T : finType) (P : pred T) : card' (@Finite.enum _) P = #|P|.
@@ -245,7 +245,7 @@ Global Instance refines_enum_boolF2 :
 Proof.
 rewrite -enumT; refines_trans; last first.
   by rewrite refinesE; do !constructor.
-rewrite refinesE /= uniq_perm_eq ?enum_uniq //.
+rewrite refinesE /= uniq_perm ?enum_uniq //.
 by move=> i; rewrite mem_enum /= !inE; case: i => [[|[|[]]] ?].
 Qed.
 
@@ -266,7 +266,7 @@ Lemma enum_npolyE (n : nat) (R : finRingType) s :
   perm_eq (Finite.enum [finType of {poly_n R}])
                (enum_npoly n iter s (@npoly_of_seq _ _)).
 Proof.
-rewrite -!enumT => Rs; rewrite uniq_perm_eq ?enum_uniq //=.
+rewrite -!enumT => Rs; rewrite uniq_perm ?enum_uniq //=.
   admit.
 move=> /= p; symmetry; rewrite mem_enum inE /=.
 apply/mapP => /=; exists p; last first.
@@ -333,4 +333,4 @@ rewrite -[[forall _, _]]/(_ == _) /= /Pdiv.Ring.rdvdp.
 by coqeal.
 Qed.
 
-End LaurentsProblem.
+End LaurentsProblem.
diff --git a/refinements/multipoly.v b/refinements/multipoly.v
@@ -1014,7 +1014,7 @@ apply (path.eq_sorted (leT:=mnmc_le)).
     by rewrite -/l Hl in_cons; apply/orP; right; rewrite mem_nth. }
   apply refine_multinom_of_seqmultinom_val, Hs.
   by rewrite -/l Hl in_cons; apply/orP; right; rewrite mem_nth. }
-apply uniq_perm_eq.
+apply uniq_perm.
 { rewrite path.sort_uniq; apply msupp_uniq. }
 { change (fun _ => multinom_of_seqmultinom_val _ _)
   with ((fun m => multinom_of_seqmultinom_val n m) \o (fst (B:=T))).
@@ -1306,7 +1306,7 @@ have -> : \sum_(m <- msupp p) f m p@_m
   = f m c + \sum_(m <- msupp pmcm) f m pmcm@_m.
 { case_eq (m \in msupp p) => Hmsuppp.
   { rewrite (big_rem _ Hmsuppp) /= Hc; f_equal.
-    rewrite /pmcm /cm -Hc -(eq_big_perm _ (msupp_rem p m)) /=.
+    rewrite /pmcm /cm -Hc -(perm_big _ (msupp_rem p m)) /=.
     apply eq_big_seq => i.
     rewrite mcoeffB mcoeffZ mcoeffX.
     rewrite mcoeff_msupp Hc -/cm -/pmcm -Hpmcm.
@@ -1426,7 +1426,7 @@ have->: sum = p0 + \big[+%R/0]_(i2 <- msupp pmpk) ((c * pmpk@_i2) *: 'X_[(m + i2
 { rewrite /sum /pmpk /p0.
   case_eq (k \in msupp p) => Hmsuppp.
   { rewrite (big_rem _ Hmsuppp) /= Hp; f_equal.
-    rewrite -Hp -(eq_big_perm _ (msupp_rem p k)) /=.
+    rewrite -Hp -(perm_big _ (msupp_rem p k)) /=.
     apply eq_big_seq => i.
     rewrite mcoeffB mcoeffZ mcoeffX.
     rewrite mcoeff_msupp Hp -Hpmpk.

diff --git a/refinements/rational.v b/refinements/rational.v
@@ -359,10 +359,10 @@ Qed.
 End Qparametric.
 End Qint.
 
-Section tests.
-
 Require Import binnat binint.
 
+Section tests.
+
 Goal (0 == 0 :> rat).
 by coqeal.
 Abort.

diff --git a/refinements/seqmx.v b/refinements/seqmx.v
@@ -1370,11 +1370,11 @@ End seqmx_poly.
 
 End seqmx_theory.
 
-Section testmx.
-
 From mathcomp Require Import ssrint poly.
 From CoqEAL Require Import binint seqpoly binord.
 
+Section testmx.
+
 Goal ((0 : 'M[int]_(2,2)) == 0).
 by coqeal.
 Abort.

diff --git a/refinements/seqmx_complements.v b/refinements/seqmx_complements.v
@@ -90,6 +90,8 @@ End seqmx_op.
 
 (** ** Refinement proofs *)
 
+Require Import Equivalence RelationClasses Morphisms.
+
 Section seqmx_theory.
 
 Context {A : Type}.
@@ -159,8 +161,6 @@ case: j IHs => [|j] IHs //=; case: k IHs => [|k] IHs //=.
 by rewrite size_store_aux.
 Qed.
 
-Require Import Equivalence RelationClasses Morphisms.
-
 Global Instance store_ssr : store_of A ordinal (matrix A) :=
   fun m n (M : 'M[A]_(m, n)) (i : 'I_m) (j : 'I_n) v =>
   \matrix_(i', j')

diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v
@@ -653,11 +653,11 @@ End seqpoly_theory.
 Hint Extern 0 (refines _ (Poly _) _) => simpl : typeclass_instances.
 Hint Extern 0 (refines _ _ (Poly _)) => simpl : typeclass_instances.
 
-Section testpoly.
-
 From mathcomp Require Import ssrint.
 From CoqEAL Require Import binnat binint.
 
+Section testpoly.
+
 Goal (0 == 0 :> {poly int}).
 by coqeal.
 Abort.

diff --git a/theory/bareiss.v b/theory/bareiss.v
@@ -53,6 +53,8 @@ Qed.
 
 End prelude.
 
+Require Import polydvd.
+
 Module poly.
 Section bareiss.
 
@@ -412,8 +414,6 @@ End Bareiss2.
   In practice, we apply this algorithm to the characteristic matrix
   so we get the characteristic polynomial in polynomial time
 *)
-Require Import polydvd.
-
 Import PolyDvdRing.
 
 Section bareiss_det.
@@ -462,5 +462,3 @@ Qed.
 
 End bareiss_det.
 End dvdring.
-
-
diff --git a/theory/edr.v b/theory/edr.v
@@ -295,12 +295,12 @@ Lemma minor_diag_mx_seq :
 Proof.
 elim: k=>[f g|j IHj f g Hf Hg Hfg]; first by rewrite /minor det_mx00 big_ord0.
 have: perm_eq [seq f x | x in 'I_j.+1] [seq g x | x in 'I_j.+1].
-  have [||e _] := leq_size_perm _ Hfg; first by rewrite map_inj_uniq ?enum_uniq.
+  have [||_ e] := uniq_min_size _ Hfg; first by rewrite map_inj_uniq ?enum_uniq.
     by rewrite !size_map.
-  by rewrite uniq_perm_eq // map_inj_uniq // enum_uniq.
+  by rewrite uniq_perm // map_inj_uniq // enum_uniq.
 have Ht : size (codom g) == j.+1 by rewrite size_codom card_ord.
 have -> : image g 'I_j.+1 = Tuple Ht by [].
-case/tuple_perm_eqP=> p Hp .
+case/tuple_permP=> p Hp .
 have Hfg0 i : g (p i) = f i.
   have He : i < #|'I_j.+1| by rewrite card_ord.
   have {2}-> : i = enum_val (Ordinal He) by rewrite enum_val_ord; apply: ord_inj.

diff --git a/theory/similar.v b/theory/similar.v
@@ -199,12 +199,12 @@ Lemma similar_diag_mx_seq m n s1 s2 :
 similar (diag_mx_seq m m s1) (diag_mx_seq n n s2).
 Proof.
 move=> eq Hms Hp.
-have Hs12:= (perm_eq_size Hp).
+have Hs12:= (perm_size Hp).
 have Hs2: size s2 == n by  rewrite -Hs12 Hms eq.
 pose t:= Tuple Hs2.
 have HE: s2 = t by [].
 move: Hp; rewrite HE.
-case/tuple_perm_eqP=> p Hp.
+case/tuple_permP=> p Hp.
 split=> //; rewrite eq.
 exists (perm_mx p)^T; split; first by rewrite unitmx_tr unitmx_perm.
 apply/matrixP=> i j; rewrite conform_mx_id !mxE (bigD1 j) //= big1 ?addr0.