Change Implicit Arguments to Arguments in algebra

13 files changed, 175 insertions, 176 deletions

diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 3a50934..7a1cacf 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -62,8 +62,7 @@ Definition gen_pack T :=
 
 End Generic.
 
-Implicit Arguments
-  gen_pack [type base_type class_of base_of to_choice base_sort].
+Arguments gen_pack [type base_type class_of base_of to_choice base_sort].
 Local Notation fin_ c := (@Finite.Class _ c c).
 Local Notation do_pack pack T := (pack T _ _ id _ _ id).
 Import GRing.Theory.
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index a85b3ec..e043561 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -186,11 +186,11 @@ rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gtr_eqF // addrC.
 rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gtr_eqF //=.
 by rewrite ltr_pmul2l ?ltz_pmod.
 Qed.
-Implicit Arguments divzMpl [p m d].
+Arguments divzMpl [p m d].
 
 Lemma divzMpr p m d : p > 0 -> (m * p %/ (d * p) = m %/ d)%Z.
 Proof. by move=> p_gt0; rewrite -!(mulrC p) divzMpl. Qed.
-Implicit Arguments divzMpr [p m d].
+Arguments divzMpr [p m d].
 
 Lemma lez_floor m d : d != 0 -> (m %/ d)%Z * d <= m.
 Proof. by rewrite -subr_ge0; apply: modz_ge0. Qed.
@@ -340,14 +340,14 @@ apply: (iffP dvdnP) => [] [q Dm]; last by exists `|q|%N; rewrite Dm abszM.
 exists ((-1) ^+ (m < 0)%R * q%:Z * (-1) ^+ (d < 0)%R).
 by rewrite -!mulrA -abszEsign -PoszM -Dm -intEsign.
 Qed.
-Implicit Arguments dvdzP [d m].
+Arguments dvdzP [d m].
 
 Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
 Proof.
 apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl.
 by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z.
 Qed.
-Implicit Arguments dvdz_mod0P [d m].
+Arguments dvdz_mod0P [d m].
 
 Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z * d == m).
 Proof. by rewrite (sameP dvdz_mod0P eqP) subr_eq0 eq_sym. Qed.
@@ -408,11 +408,11 @@ Proof. by rewrite -!(mulrC p); apply: divzMl. Qed.
 
 Lemma dvdz_mul2l p d m : p != 0 -> (p * d %| p * m)%Z = (d %| m)%Z.
 Proof. by rewrite !dvdzE -absz_gt0 !abszM; apply: dvdn_pmul2l. Qed.
-Implicit Arguments dvdz_mul2l [p m d].
+Arguments dvdz_mul2l [p d m].
 
 Lemma dvdz_mul2r p d m : p != 0 -> (d * p %| m * p)%Z = (d %| m)%Z.
 Proof. by rewrite !dvdzE -absz_gt0 !abszM; apply: dvdn_pmul2r. Qed.
-Implicit Arguments dvdz_mul2r [p m d].
+Arguments dvdz_mul2r [p d m].
 
 Lemma dvdz_exp2l p m n : (m <= n)%N -> (p ^+ m %| p ^+ n)%Z.
 Proof. by rewrite dvdzE !abszX; apply: dvdn_exp2l. Qed.
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index e269752..b699da1 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -134,7 +134,7 @@ Lemma itv_dec : forall (x : R) (i : interval R),
   reflect (itv_decompose i x) (x \in i).
 Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed.
 
-Implicit Arguments itv_dec [x i].
+Arguments itv_dec [x i].
 
 Definition lersif (x y : R) b := if b then x < y else x <= y.
 
@@ -243,7 +243,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
 Qed.
 
 Hint Rewrite intP.
-Implicit Arguments itvP [x i].
+Arguments itvP [x i].
 
 Definition subitv (i1 i2 : interval R) :=
   match i1, i2 with
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index aecbce9..b54e586 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -306,7 +306,7 @@ Variable R : Type.
 (* Constant matrix *)
 Fact const_mx_key : unit. Proof. by []. Qed.
 Definition const_mx m n a : 'M[R]_(m, n) := \matrix[const_mx_key]_(i, j) a.
-Implicit Arguments const_mx [[m] [n]].
+Arguments const_mx {m n}.
 
 Section FixedDim.
 (* Definitions and properties for which we can work with fixed dimensions. *)
@@ -911,10 +911,10 @@ End VecMatrix.
 
 End MatrixStructural.
 
-Implicit Arguments const_mx [R m n].
-Implicit Arguments row_mxA [R m n1 n2 n3 A1 A2 A3].
-Implicit Arguments col_mxA [R m1 m2 m3 n A1 A2 A3].
-Implicit Arguments block_mxA
+Arguments const_mx [R m n].
+Arguments row_mxA [R m n1 n2 n3 A1 A2 A3].
+Arguments col_mxA [R m1 m2 m3 n A1 A2 A3].
+Arguments block_mxA
   [R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33].
 Prenex Implicits const_mx castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx.
 Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx.
@@ -2042,19 +2042,19 @@ Definition adjugate n (A : 'M_n) := \matrix[adjugate_key]_(i, j) cofactor A j i.
 
 End MatrixAlgebra.
 
-Implicit Arguments delta_mx [R m n].
-Implicit Arguments scalar_mx [R n].
-Implicit Arguments perm_mx [R n].
-Implicit Arguments tperm_mx [R n].
-Implicit Arguments pid_mx [R m n].
-Implicit Arguments copid_mx [R n].
-Implicit Arguments lin_mulmxr [R m n p].
+Arguments delta_mx [R m n].
+Arguments scalar_mx [R n].
+Arguments perm_mx [R n].
+Arguments tperm_mx [R n].
+Arguments pid_mx [R m n].
+Arguments copid_mx [R n].
+Arguments lin_mulmxr [R m n p].
 Prenex Implicits delta_mx diag_mx scalar_mx is_scalar_mx perm_mx tperm_mx.
 Prenex Implicits pid_mx copid_mx mulmx lin_mulmxr.
 Prenex Implicits mxtrace determinant cofactor adjugate.
 
-Implicit Arguments is_scalar_mxP [R n A].
-Implicit Arguments mul_delta_mx [R m n p].
+Arguments is_scalar_mxP [R n A].
+Arguments mul_delta_mx [R m n p].
 Prenex Implicits mul_delta_mx.
 
 Notation "a %:M" := (scalar_mx a) : ring_scope.
@@ -2496,8 +2496,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed.
 
 End ComMatrix.
 
-Implicit Arguments lin_mul_row [R m n].
-Implicit Arguments lin_mulmx [R m n p].
+Arguments lin_mul_row [R m n].
+Arguments lin_mulmx [R m n p].
 Prenex Implicits lin_mul_row lin_mulmx.
 
 Canonical matrix_finAlgType (R : finComRingType) n' :=
@@ -2779,7 +2779,7 @@ Qed.
 
 End MatrixDomain.
 
-Implicit Arguments det0P [R n A].
+Arguments det0P [R n A].
 
 (* Parametricity at the field level (mx_is_scalar, unit and inverse are only *)
 (* mapped at this level).                                                    *)
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 463f07b..9cf3f6e 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -432,7 +432,7 @@ Proof. by rewrite mulmxA -[col_base A *m _]mulmxA pid_mx_id ?mulmx_ebase. Qed.
 Lemma mulmx1_min_rank r m n (A : 'M_(m, n)) M N :
   M *m A *m N = 1%:M :> 'M_r -> r <= \rank A.
 Proof. by rewrite -{1}(mulmx_base A) mulmxA -mulmxA; move/mulmx1_min. Qed.
-Implicit Arguments mulmx1_min_rank [r m n A].
+Arguments mulmx1_min_rank [r m n A].
 
 Lemma mulmx_max_rank r m n (M : 'M_(m, r)) (N : 'M_(r, n)) :
   \rank (M *m N) <= r.
@@ -444,7 +444,7 @@ suffices: L *m M *m (N *m U) = 1%:M by apply: mulmx1_min.
 rewrite mulmxA -(mulmxA L) -[M *m N]mulmx_ebase -/MN.
 by rewrite !mulmxA mulmxKV // mulmxK // !pid_mx_id /rMN ?pid_mx_1.
 Qed.
-Implicit Arguments mulmx_max_rank [r m n].
+Arguments mulmx_max_rank [r m n].
 
 Lemma mxrank_tr m n (A : 'M_(m, n)) : \rank A^T = \rank A.
 Proof.
@@ -511,7 +511,7 @@ Proof.
 apply: (iffP idP) => [/mulmxKpV | [D ->]]; first by exists (A *m pinvmx B).
 by rewrite submxE -mulmxA mulmx_coker mulmx0.
 Qed.
-Implicit Arguments submxP [m1 m2 n A B].
+Arguments submxP [m1 m2 n A B].
 
 Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS.
 Proof. by rewrite submxE mulmx_coker. Qed.
@@ -612,7 +612,7 @@ apply: (iffP idP) => [sAB i|sAB].
 rewrite submxE; apply/eqP/row_matrixP=> i; apply/eqP.
 by rewrite row_mul row0 -submxE.
 Qed.
-Implicit Arguments row_subP [m1 m2 n A B].
+Arguments row_subP [m1 m2 n A B].
 
 Lemma rV_subP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (forall v : 'rV_n, v <= A -> v <= B)%MS (A <= B)%MS.
@@ -620,7 +620,7 @@ Proof.
 apply: (iffP idP) => [sAB v Av | sAB]; first exact: submx_trans sAB.
 by apply/row_subP=> i; rewrite sAB ?row_sub.
 Qed.
-Implicit Arguments rV_subP [m1 m2 n A B].
+Arguments rV_subP [m1 m2 n A B].
 
 Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS).
@@ -668,7 +668,7 @@ apply: (iffP idP) => [Afull | [B kA]].
   by exists (1%:M *m pinvmx A); apply: mulmxKpV (submx_full _ Afull).
 by rewrite [_ A]eqn_leq rank_leq_col (mulmx1_min_rank B 1%:M) ?mulmx1.
 Qed.
-Implicit Arguments row_fullP [m n A].
+Arguments row_fullP [m n A].
 
 Lemma row_full_inj m n p A : row_full A -> injective (@mulmx _ m n p A).
 Proof.
@@ -739,7 +739,7 @@ split=> [|m3 C]; first by apply/eqP; rewrite eqn_leq !mxrankS.
 split; first by apply/idP/idP; apply: submx_trans.
 by apply/idP/idP=> sC; apply: submx_trans sC _.
 Qed.
-Implicit Arguments eqmxP [m1 m2 n A B].
+Arguments eqmxP [m1 m2 n A B].
 
 Lemma rV_eqP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (forall u : 'rV_n, (u <= A) = (u <= B))%MS (A == B)%MS.
@@ -860,7 +860,7 @@ Proof.
 apply: (iffP idP) => eqAB; first exact: eq_genmx (eqmxP _).
 by rewrite -!(genmxE A) eqAB !genmxE andbb.
 Qed.
-Implicit Arguments genmxP [m1 m2 n A B].
+Arguments genmxP [m1 m2 n A B].
 
 Lemma genmx0 m n : <<0 : 'M_(m, n)>>%MS = 0.
 Proof. by apply/eqP; rewrite -submx0 genmxE sub0mx. Qed.
@@ -1066,7 +1066,7 @@ apply: (iffP idP) => [|[u ->]]; last by rewrite addmx_sub_adds ?submxMl.
 rewrite addsmxE; case/submxP=> u ->; exists (lsubmx u, rsubmx u).
 by rewrite -mul_row_col hsubmxK.
 Qed.
-Implicit Arguments sub_addsmxP [m1 m2 m3 n A B C].
+Arguments sub_addsmxP [m1 m2 m3 n A B C].
 
 Variable I : finType.
 Implicit Type P : pred I.
@@ -1080,7 +1080,7 @@ Lemma sumsmx_sup i0 P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) :
 Proof.
 by move=> Pi0 sAB; apply: submx_trans sAB _; rewrite (bigD1 i0) // addsmxSl.
 Qed.
-Implicit Arguments sumsmx_sup [P m n A B_].
+Arguments sumsmx_sup i0 [P m n A B_].
 
 Lemma sumsmx_subP P m n (A_ : I -> 'M_n) (B : 'M_(m, n)) :
   reflect (forall i, P i -> A_ i <= B)%MS (\sum_(i | P i) A_ i <= B)%MS.
@@ -1790,7 +1790,7 @@ Notation mxdirect A := (mxdirect_def (Phantom 'M_(_,_) A%MS)).
 Lemma mxdirectP n (S : proper_mxsum_expr n) :
   reflect (\rank S = proper_mxsum_rank S) (mxdirect S).
 Proof. exact: eqnP. Qed.
-Implicit Arguments mxdirectP [n S].
+Arguments mxdirectP [n S].
 
 Lemma mxdirect_trivial m n A : mxdirect (unwrap (@trivial_mxsum m n A)).
 Proof. exact: eqxx. Qed.
@@ -1972,38 +1972,38 @@ End Eigenspace.
 End RowSpaceTheory.
 
 Hint Resolve submx_refl.
-Implicit Arguments submxP [F m1 m2 n A B].
-Implicit Arguments eq_row_sub [F m n v A].
-Implicit Arguments row_subP [F m1 m2 n A B].
-Implicit Arguments rV_subP [F m1 m2 n A B].
-Implicit Arguments row_subPn [F m1 m2 n A B].
-Implicit Arguments sub_rVP [F n u v].
-Implicit Arguments rV_eqP [F m1 m2 n A B].
-Implicit Arguments rowV0Pn [F m n A].
-Implicit Arguments rowV0P [F m n A].
-Implicit Arguments eqmx0P [F m n A].
-Implicit Arguments row_fullP [F m n A].
-Implicit Arguments row_freeP [F m n A].
-Implicit Arguments eqmxP [F m1 m2 n A B].
-Implicit Arguments genmxP [F m1 m2 n A B].
-Implicit Arguments addsmx_idPr [F m1 m2 n A B].
-Implicit Arguments addsmx_idPl [F m1 m2 n A B].
-Implicit Arguments sub_addsmxP [F m1 m2 m3 n A B C].
-Implicit Arguments sumsmx_sup [F I P m n A B_].
-Implicit Arguments sumsmx_subP [F I P m n A_ B].
-Implicit Arguments sub_sumsmxP [F I P m n A B_].
-Implicit Arguments sub_kermxP [F p m n A B].
-Implicit Arguments capmx_idPr [F m1 m2 n A B].
-Implicit Arguments capmx_idPl [F m1 m2 n A B].
-Implicit Arguments bigcapmx_inf [F I P m n A_ B].
-Implicit Arguments sub_bigcapmxP [F I P m n A B_].
-Implicit Arguments mxrank_injP [F m n A f].
-Implicit Arguments mxdirectP [F n S].
-Implicit Arguments mxdirect_addsP [F m1 m2 n A B].
-Implicit Arguments mxdirect_sumsP [F I P n A_].
-Implicit Arguments mxdirect_sumsE [F I P n S_].
-Implicit Arguments eigenspaceP [F n g a m W].
-Implicit Arguments eigenvalueP [F n g a].
+Arguments submxP [F m1 m2 n A B].
+Arguments eq_row_sub [F m n v A].
+Arguments row_subP [F m1 m2 n A B].
+Arguments rV_subP [F m1 m2 n A B].
+Arguments row_subPn [F m1 m2 n A B].
+Arguments sub_rVP [F n u v].
+Arguments rV_eqP [F m1 m2 n A B].
+Arguments rowV0Pn [F m n A].
+Arguments rowV0P [F m n A].
+Arguments eqmx0P [F m n A].
+Arguments row_fullP [F m n A].
+Arguments row_freeP [F m n A].
+Arguments eqmxP [F m1 m2 n A B].
+Arguments genmxP [F m1 m2 n A B].
+Arguments addsmx_idPr [F m1 m2 n A B].
+Arguments addsmx_idPl [F m1 m2 n A B].
+Arguments sub_addsmxP [F m1 m2 m3 n A B C].
+Arguments sumsmx_sup [F I] i0 [P m n A B_].
+Arguments sumsmx_subP [F I P m n A_ B].
+Arguments sub_sumsmxP [F I P m n A B_].
+Arguments sub_kermxP [F p m n A B].
+Arguments capmx_idPr [F n m1 m2 A B].
+Arguments capmx_idPl [F n m1 m2 A B].
+Arguments bigcapmx_inf [F I] i0 [P m n A_ B].
+Arguments sub_bigcapmxP [F I P m n A B_].
+Arguments mxrank_injP [F m n] p [A f].
+Arguments mxdirectP [F n S].
+Arguments mxdirect_addsP [F m1 m2 n A B].
+Arguments mxdirect_sumsP [F I P n A_].
+Arguments mxdirect_sumsE [F I P n S_].
+Arguments eigenspaceP [F n g a m W].
+Arguments eigenvalueP [F n g a].
 
 Arguments Scope mxrank [_ nat_scope nat_scope matrix_set_scope].
 Arguments Scope complmx [_ nat_scope nat_scope matrix_set_scope].
@@ -2241,7 +2241,7 @@ Proof.
 apply: (iffP idP) => [sR12 A R1_A | sR12]; first exact: submx_trans sR12.
 by apply/rV_subP=> vA; rewrite -(vec_mxK vA); apply: sR12.
 Qed.
-Implicit Arguments memmx_subP [m1 m2 n R1 R2].
+Arguments memmx_subP [m1 m2 n R1 R2].
 
 Lemma memmx_eqP m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
   reflect (forall A, (A \in R1) = (A \in R2)) (R1 == R2)%MS.
@@ -2249,7 +2249,7 @@ Proof.
 apply: (iffP eqmxP) => [eqR12 A | eqR12]; first by rewrite eqR12.
 by apply/eqmxP; apply/rV_eqP=> vA; rewrite -(vec_mxK vA) eqR12.
 Qed.
-Implicit Arguments memmx_eqP [m1 m2 n R1 R2].
+Arguments memmx_eqP [m1 m2 n R1 R2].
 
 Lemma memmx_addsP m1 m2 n A (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) :
   reflect (exists D, [/\ D.1 \in R1, D.2 \in R2 & A = D.1 + D.2])
@@ -2261,7 +2261,7 @@ apply: (iffP sub_addsmxP) => [[u /(canRL mxvecK)->] | [D []]].
 case/submxP=> u1 defD1 /submxP[u2 defD2] ->.
 by exists (u1, u2); rewrite linearD /= defD1 defD2.
 Qed.
-Implicit Arguments memmx_addsP [m1 m2 n A R1 R2].
+Arguments memmx_addsP [m1 m2 n A R1 R2].
 
 Lemma memmx_sumsP (I : finType) (P : pred I) n (A : 'M_n) R_ :
   reflect (exists2 A_, A = \sum_(i | P i) A_ i & forall i, A_ i \in R_ i)
@@ -2274,7 +2274,7 @@ apply: (iffP sub_sumsmxP) => [[C defA] | [A_ -> R_A] {A}].
 exists (fun i => mxvec (A_ i) *m pinvmx (R_ i)).
 by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV.
 Qed.
-Implicit Arguments memmx_sumsP [I P n A R_].
+Arguments memmx_sumsP [I P n A R_].
 
 Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : 
     (1%:M \in R)%MS ->
@@ -2325,7 +2325,7 @@ case/memmx_sumsP=> A_ -> R_A; rewrite linear_sum summx_sub //= => j _.
 rewrite (submx_trans (R_A _)) // genmxE; apply/row_subP=> i.
 by rewrite row_mul mul_rV_lin sR12R ?vec_mxK ?row_sub.
 Qed.
-Implicit Arguments mulsmx_subP [m1 m2 m n R1 R2 R].
+Arguments mulsmx_subP [m1 m2 m n R1 R2 R].
 
 Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n))
                             (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) :
@@ -2360,7 +2360,7 @@ exists A2_ => [i|]; first by rewrite vec_mxK -(genmxE R2) row_sub.
 apply: eq_bigr => i _; rewrite -[_ *m _](mx_rV_lin (mulmxr_linear _ _)).
 by rewrite -mulmxA mulmxKpV ?mxvecK // -(genmxE (_ *m _)) R_A.
 Qed.
-Implicit Arguments mulsmxP [m1 m2 n A R1 R2].
+Arguments mulsmxP [m1 m2 n A R1 R2].
 
 Lemma mulsmxA m1 m2 m3 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
   (R1 * (R2 * R3) = R1 * R2 * R3)%MS.
@@ -2450,7 +2450,7 @@ congr (row_mx 0 (row_mx (mxvec _) (mxvec _))); apply/row_matrixP=> i.
   by rewrite !row_mul !mul_rV_lin1 /= mxvecK ideR vec_mxK ?row_sub.
 by rewrite !row_mul !mul_rV_lin1 /= mxvecK idRe vec_mxK ?row_sub.
 Qed.
-Implicit Arguments mxring_idP [m n R].
+Arguments mxring_idP [m n R].
 
 Section CentMxDef.
 
@@ -2486,7 +2486,7 @@ apply: (iffP sub_kermxP); rewrite mul_vec_lin => cBE.
 apply: (canLR vec_mxK); apply/row_matrixP=> i.
 by rewrite row_mul mul_rV_lin /= cBE subrr !linear0.
 Qed.
-Implicit Arguments cent_rowP [m n B R].
+Arguments cent_rowP [m n B R].
 
 Lemma cent_mxP m n B (R : 'A_(m, n)) :
   reflect (forall A, A \in R -> A *m B = B *m A) (B \in 'C(R))%MS.
@@ -2497,7 +2497,7 @@ apply: (iffP cent_rowP) => cEB => [A sAE | i A].
   by rewrite !linearZ -scalemxAl /= cEB.
 by rewrite cEB // vec_mxK row_sub.
 Qed.
-Implicit Arguments cent_mxP [m n B R].
+Arguments cent_mxP [m n B R].
 
 Lemma scalar_mx_cent m n a (R : 'A_(m, n)) : (a%:M \in 'C(R))%MS.
 Proof. by apply/cent_mxP=> A _; apply: scalar_mxC. Qed.
@@ -2512,7 +2512,7 @@ Proof.
 rewrite sub_capmx; case R_A: (A \in R); last by right; case.
 by apply: (iffP cent_mxP) => [cAR | [_ cAR]].
 Qed.
-Implicit Arguments center_mxP [m n A R].
+Arguments center_mxP [m n A R].
 
 Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 :
   mxring_id R e1 -> mxring_id R e2 -> e1 = e2.
@@ -2634,16 +2634,16 @@ Notation "''C_' R ( S )" := (R :&: 'C(S))%MS : matrix_set_scope.
 Notation "''C_' ( R ) ( S )" := ('C_R(S))%MS (only parsing) : matrix_set_scope.
 Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope.
 
-Implicit Arguments memmx_subP [F m1 m2 n R1 R2].
-Implicit Arguments memmx_eqP [F m1 m2 n R1 R2].
-Implicit Arguments memmx_addsP [F m1 m2 n R1 R2].
-Implicit Arguments memmx_sumsP [F I P n A R_].
-Implicit Arguments mulsmx_subP [F m1 m2 m n R1 R2 R].
-Implicit Arguments mulsmxP [F m1 m2 n A R1 R2].
-Implicit Arguments mxring_idP [m n R].
-Implicit Arguments cent_rowP [F m n B R].
-Implicit Arguments cent_mxP [F m n B R].
-Implicit Arguments center_mxP [F m n A R].
+Arguments memmx_subP [F m1 m2 n R1 R2].
+Arguments memmx_eqP [F m1 m2 n R1 R2].
+Arguments memmx_addsP [F m1 m2 n] A [R1 R2].
+Arguments memmx_sumsP [F I P n A R_].
+Arguments mulsmx_subP [F m1 m2 m n R1 R2 R].
+Arguments mulsmxP [F m1 m2 n A R1 R2].
+Arguments mxring_idP F [m n R].
+Arguments cent_rowP [F m n B R].
+Arguments cent_mxP [F m n B R].
+Arguments center_mxP [F m n A R].
 
 (* Parametricity for the row-space/F-algebra theory.                         *)
 Section MapMatrixSpaces.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 4d043ea..5f83ab0 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -115,7 +115,7 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear.
 
 End RowPoly.
 
-Implicit Arguments poly_rV [R d].
+Arguments poly_rV [R d].
 Prenex Implicits rVpoly poly_rV.
 
 Section Resultant.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 5e684a1..409930c 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -1662,7 +1662,7 @@ Qed.
 End PolynomialTheory.
 
 Prenex Implicits polyC Poly lead_coef root horner polyOver.
-Implicit Arguments monic [[R]].
+Arguments monic {R}.
 Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope.
 Notation "c %:P" := (polyC c) : ring_scope.
 Notation "'X" := (polyX _) : ring_scope.
@@ -1674,12 +1674,12 @@ Notation "a ^` ()" := (deriv a) : ring_scope.
 Notation "a ^` ( n )" := (derivn n a) : ring_scope.
 Notation "a ^`N ( n )" := (nderivn n a) : ring_scope.
 
-Implicit Arguments monicP [R p].
-Implicit Arguments rootP [R p x].
-Implicit Arguments rootPf [R p x].
-Implicit Arguments rootPt [R p x].
-Implicit Arguments unity_rootP [R n z].
-Implicit Arguments polyOverP [[R] [S0] [addS] [kS] [p]].
+Arguments monicP [R p].
+Arguments rootP [R p x].
+Arguments rootPf [R p x].
+Arguments rootPt [R p x].
+Arguments unity_rootP [R n z].
+Arguments polyOverP {R S0 addS kS p}.
 
 (* Container morphism. *)
 Section MapPoly.
@@ -2342,7 +2342,7 @@ Qed.
 
 End MapFieldPoly.
 
-Implicit Arguments map_poly_inj [[F] [R] x1 x2].
+Arguments map_poly_inj {F R} f [x1 x2].
 
 Section MaxRoots.
 
@@ -2523,7 +2523,7 @@ Open Scope unity_root_scope.
 
 Definition unity_rootE := unity_rootE.
 Definition unity_rootP := @unity_rootP.
-Implicit Arguments unity_rootP [R n z].
+Arguments unity_rootP [R n z].
 
 Definition prim_order_exists := prim_order_exists.
 Notation prim_order_gt0 :=  prim_order_gt0.
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 393b37b..cd7d306 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -777,7 +777,7 @@ Qed.
 
 End InPrealField.
 
-Implicit Arguments ratr [[R]].
+Arguments ratr {R}.
 
 (* Conntecting rationals to the ring an field tactics *)
 
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 9a0314e..1725e5e 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -859,9 +859,9 @@ End ClosedPredicates.
 
 End ZmoduleTheory.
 
-Implicit Arguments addrI [[V] x1 x2].
-Implicit Arguments addIr [[V] x1 x2].
-Implicit Arguments oppr_inj [[V] x1 x2].
+Arguments addrI {V} y [x1 x2].
+Arguments addIr {V} x [x1 x2].
+Arguments oppr_inj {V} [x1 x2].
 
 Module Ring.
 
@@ -2476,7 +2476,7 @@ End ClassDef.
 
 Module Exports.
 Coercion base : class_of >-> Ring.class_of.
-Implicit Arguments mixin [R].
+Arguments mixin [R].
 Coercion mixin : class_of >-> commutative.
 Coercion sort : type >-> Sortclass.
 Bind Scope ring_scope with sort.
@@ -3016,7 +3016,7 @@ End ClosedPredicates.
 
 End UnitRingTheory.
 
-Implicit Arguments invr_inj [[R] x1 x2].
+Arguments invr_inj {R} [x1 x2].
 
 Section UnitRingMorphism.
 
@@ -3740,7 +3740,7 @@ Arguments Scope Not [_ term_scope].
 Arguments Scope Exists [_ nat_scope term_scope].
 Arguments Scope Forall [_ nat_scope term_scope].
 
-Implicit Arguments Bool [R].
+Arguments Bool [R].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
 Prenex Implicits Exists Forall.
 
@@ -4363,7 +4363,7 @@ End ClassDef.
 
 Module Exports.
 Coercion base : class_of >-> ComUnitRing.class_of.
-Implicit Arguments mixin [R x y].
+Arguments mixin [R] c [x y].
 Coercion mixin : class_of >-> axiom.
 Coercion sort : type >-> Sortclass.
 Bind Scope ring_scope with sort.
@@ -4511,8 +4511,8 @@ Canonical regular_idomainType := [idomainType of R^o].
 
 End IntegralDomainTheory.
 
-Implicit Arguments lregP [[R] [x]].
-Implicit Arguments rregP [[R] [x]].
+Arguments lregP {R x}.
+Arguments rregP {R x}.
 
 Module Field.
 
@@ -4580,7 +4580,7 @@ End ClassDef.
 
 Module Exports.
 Coercion base : class_of >-> IntegralDomain.class_of.
-Implicit Arguments mixin [F x].
+Arguments mixin [F] c [x].
 Coercion mixin : class_of >-> mixin_of.
 Coercion sort : type >-> Sortclass.
 Bind Scope ring_scope with sort.
@@ -4794,7 +4794,7 @@ End Predicates.
 
 End FieldTheory.
 
-Implicit Arguments fmorph_inj [[F] [R] x1 x2].
+Arguments fmorph_inj {F R} f [x1 x2].
 
 Module DecidableField.
 
@@ -4928,8 +4928,8 @@ Qed.
 
 End DecidableFieldTheory.
 
-Implicit Arguments satP [[F] [e] [f]].
-Implicit Arguments solP [[F] [n] [f]].
+Arguments satP {F e f}.
+Arguments solP {F n f}.
 
 Section QE_Mixin.
 
@@ -5349,13 +5349,13 @@ Definition addrI := @addrI.
 Definition addIr := @addIr.
 Definition subrI := @subrI.
 Definition subIr := @subIr.
-Implicit Arguments addrI [[V] x1 x2].
-Implicit Arguments addIr [[V] x1 x2].
-Implicit Arguments subrI [[V] x1 x2].
-Implicit Arguments subIr [[V] x1 x2].
+Arguments addrI {V} y [x1 x2].
+Arguments addIr {V} x [x1 x2].
+Arguments subrI {V} y [x1 x2].
+Arguments subIr {V} x [x1 x2].
 Definition opprK := opprK.
 Definition oppr_inj := @oppr_inj.
-Implicit Arguments oppr_inj [[V] x1 x2].
+Arguments oppr_inj {V} [x1 x2].
 Definition oppr0 := oppr0.
 Definition oppr_eq0 := oppr_eq0.
 Definition opprD := opprD.
@@ -5539,7 +5539,7 @@ Definition commrV := commrV.
 Definition unitrE := unitrE.
 Definition invrK := invrK.
 Definition invr_inj := @invr_inj.
-Implicit Arguments invr_inj [[R] x1 x2].
+Arguments invr_inj {R} [x1 x2].
 Definition unitrV := unitrV.
 Definition unitr1 := unitr1.
 Definition invr1 := invr1.
@@ -5702,7 +5702,7 @@ Definition rmorphV := rmorphV.
 Definition rmorph_div := rmorph_div.
 Definition fmorph_eq0 := fmorph_eq0.
 Definition fmorph_inj := @fmorph_inj.
-Implicit Arguments fmorph_inj [[F] [R] x1 x2].
+Arguments fmorph_inj {F R} f [x1 x2].
 Definition fmorph_eq1 := fmorph_eq1.
 Definition fmorph_char := fmorph_char.
 Definition fmorph_unit := fmorph_unit.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index e6c4ca6..752be45 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -970,7 +970,7 @@ End NumMorphism.
 
 End MorphTheory.
 
-Implicit Arguments intr_inj [[R] x1 x2].
+Arguments intr_inj {R} [x1 x2].
 
 Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
   match n with
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 219f804..0d9d135 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1251,11 +1251,11 @@ Definition normrE x := (normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0,
 
 End NumIntegralDomainTheory.
 
-Implicit Arguments ler01 [R].
-Implicit Arguments ltr01 [R].
-Implicit Arguments normr_idP [R x].
-Implicit Arguments normr0P [R x].
-Implicit Arguments lerifP [R x y C].
+Arguments ler01 [R].
+Arguments ltr01 [R].
+Arguments normr_idP [R x].
+Arguments normr0P [R x].
+Arguments lerifP [R x y C].
 Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0.
 
 Section NumIntegralDomainMonotonyTheory.
@@ -2680,7 +2680,7 @@ Lemma real_ler_normlP x y :
 Proof.
 by move=> Rx; rewrite real_ler_norml // ler_oppl; apply: (iffP andP) => [] [].
 Qed.
-Implicit Arguments real_ler_normlP [x y].
+Arguments real_ler_normlP [x y].
 
 Lemma real_eqr_norml x y :
   x \is real -> (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y).
@@ -2716,7 +2716,7 @@ Proof.
 move=> Rx; rewrite real_ltr_norml // ltr_oppl.
 by apply: (iffP (@andP _ _)); case.
 Qed.
-Implicit Arguments real_ltr_normlP [x y].
+Arguments real_ltr_normlP [x y].
 
 Lemma real_ler_normr x y : y \is real -> (x <= `|y|) = (x <= y) || (x <= - y).
 Proof.
@@ -3138,16 +3138,16 @@ Qed.
 End NumDomainOperationTheory.
 
 Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real.
-Implicit Arguments ler_sqr [[R] x y].
-Implicit Arguments ltr_sqr [[R] x y].
-Implicit Arguments signr_inj [[R] x1 x2].
-Implicit Arguments real_ler_normlP [R x y].
-Implicit Arguments real_ltr_normlP [R x y].
-Implicit Arguments lerif_refl [R x C].
-Implicit Arguments mono_in_lerif [R A f C].
-Implicit Arguments nmono_in_lerif [R A f C].
-Implicit Arguments mono_lerif [R f C].
-Implicit Arguments nmono_lerif [R f C].
+Arguments ler_sqr {R} [x y].
+Arguments ltr_sqr {R} [x y].
+Arguments signr_inj {R} [x1 x2].
+Arguments real_ler_normlP [R x y].
+Arguments real_ltr_normlP [R x y].
+Arguments lerif_refl [R x C].
+Arguments mono_in_lerif [R A f C].
+Arguments nmono_in_lerif [R A f C].
+Arguments mono_lerif [R f C].
+Arguments nmono_lerif [R f C].
 
 Section NumDomainMonotonyTheoryForReals.
 
@@ -3631,7 +3631,7 @@ Proof. exact: real_ler_norml. Qed.
 
 Lemma ler_normlP x y : reflect ((- x <= y) * (x <= y)) (`|x| <= y).
 Proof. exact: real_ler_normlP. Qed.
-Implicit Arguments ler_normlP [x y].
+Arguments ler_normlP [x y].
 
 Lemma eqr_norml x y : (`|x| == y) = ((x == y) || (x == -y)) && (0 <= y).
 Proof. exact: real_eqr_norml. Qed.
@@ -3646,7 +3646,7 @@ Definition lter_norml := (ler_norml, ltr_norml).
 
 Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y).
 Proof. exact: real_ltr_normlP. Qed.
-Implicit Arguments ltr_normlP [x y].
+Arguments ltr_normlP [x y].
 
 Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).
 Proof. by rewrite lerNgt ltr_norml negb_and -!lerNgt orbC ler_oppr. Qed.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index c4865ca..73354bf 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -303,7 +303,7 @@ Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
 Notation "<[ v ] >" := (vline v) : vspace_scope.
 Notation "<< X >>" := (span X) : vspace_scope.
 Notation "0" := (vline 0) : vspace_scope.
-Implicit Arguments fullv [[K] [vT]].
+Arguments fullv {K vT}.
 Prenex Implicits subsetv addv capv complv diffv span free basis_of.
 
 Notation "U + V" := (addv U V) : vspace_scope.
@@ -568,7 +568,7 @@ Implicit Type P : pred I.
 Lemma sumv_sup i0 P U Vs :
   P i0 -> (U <= Vs i0)%VS -> (U <= \sum_(i | P i) Vs i)%VS.
 Proof. by move=> Pi0 /subv_trans-> //; rewrite (bigD1 i0) ?addvSl. Qed.
-Implicit Arguments sumv_sup [P U Vs].
+Arguments sumv_sup i0 [P U Vs].
 
 Lemma subv_sumP {P Us V} :
   reflect (forall i, P i -> Us i <= V)%VS  (\sum_(i | P i) Us i <= V)%VS.
@@ -1223,27 +1223,27 @@ End BigSumBasis.
 End VectorTheory.
 
 Hint Resolve subvv.
-Implicit Arguments subvP [K vT U V].
-Implicit Arguments addv_idPl [K vT U V].
-Implicit Arguments addv_idPr [K vT U V].
-Implicit Arguments memv_addP [K vT U V w].
-Implicit Arguments sumv_sup [K vT I P U Vs].
-Implicit Arguments memv_sumP [K vT I P Us v].
-Implicit Arguments subv_sumP [K vT I P Us V].
-Implicit Arguments capv_idPl [K vT U V].
-Implicit Arguments capv_idPr [K vT U V].
-Implicit Arguments memv_capP [K vT U V w].
-Implicit Arguments bigcapv_inf [K vT I P Us V].
-Implicit Arguments subv_bigcapP [K vT I P U Vs].
-Implicit Arguments directvP [K vT S].
-Implicit Arguments directv_addP [K vT U V].
-Implicit Arguments directv_add_unique [K vT U V].
-Implicit Arguments directv_sumP [K vT I P Us].
-Implicit Arguments directv_sumE [K vT I P Ss].
-Implicit Arguments directv_sum_independent [K vT I P Us].
-Implicit Arguments directv_sum_unique [K vT I P Us].
-Implicit Arguments span_subvP [K vT X U].
-Implicit Arguments freeP [K vT n X].
+Arguments subvP [K vT U V].
+Arguments addv_idPl [K vT U V].
+Arguments addv_idPr [K vT U V].
+Arguments memv_addP [K vT w U V ].
+Arguments sumv_sup [K vT I] i0 [P U Vs].
+Arguments memv_sumP [K vT I P Us v].
+Arguments subv_sumP [K vT I P Us V].
+Arguments capv_idPl [K vT U V].
+Arguments capv_idPr [K vT U V].
+Arguments memv_capP [K vT w U V].
+Arguments bigcapv_inf [K vT I] i0 [P Us V].
+Arguments subv_bigcapP [K vT I P U Vs].
+Arguments directvP [K vT S].
+Arguments directv_addP [K vT U V].
+Arguments directv_add_unique [K vT U V].
+Arguments directv_sumP [K vT I P Us].
+Arguments directv_sumE [K vT I P Ss].
+Arguments directv_sum_independent [K vT I P Us].
+Arguments directv_sum_unique [K vT I P Us].
+Arguments span_subvP [K vT X U].
+Arguments freeP [K vT n X].
 
 Prenex Implicits coord.
 Notation directv S := (directv_def (Phantom _ S%VS)).
@@ -1598,11 +1598,11 @@ Proof. by move/lker0_lfunK=> fK; apply/lfunP=> u; rewrite !lfunE /= fK. Qed.
 
 End LinearImage.
 
-Implicit Arguments memv_imgP [K aT rT f U w].
-Implicit Arguments lfunPn [K aT rT f g].
-Implicit Arguments lker0P [K aT rT f].
-Implicit Arguments eqlfunP [K aT rT f g v].
-Implicit Arguments eqlfun_inP [K aT rT f g V].
+Arguments memv_imgP [K aT rT f w U].
+Arguments lfunPn [K aT rT f g].
+Arguments lker0P [K aT rT f].
+Arguments eqlfunP [K aT rT f g v].
+Arguments eqlfun_inP [K aT rT V f g].
 
 Section FixedSpace.
 
@@ -1632,8 +1632,8 @@ Qed.
 
 End FixedSpace.
 
-Implicit Arguments fixedSpaceP [K vT f a].
-Implicit Arguments fixedSpacesP [K vT f U].
+Arguments fixedSpaceP [K vT f a].
+Arguments fixedSpacesP [K vT f U].
 
 Section LinAut.
 
@@ -1943,8 +1943,8 @@ Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.
 
 End SubVector.
 Prenex Implicits vsval vsproj vsvalK.
-Implicit Arguments subvs_inj [[K] [vT] [U] x1 x2].
-Implicit Arguments vsprojK [[K] [vT] [U] x].
+Arguments subvs_inj {K vT U} [x1 x2].
+Arguments vsprojK {K vT U} [x].
 
 Section MatrixVectType.
 
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index ec9750a..f9bdaaa 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -178,9 +178,9 @@ Proof. by rewrite orderE -Zp_cycle cardsT card_ord. Qed.
 
 End ZpDef.
 
-Implicit Arguments Zp0 [[p']].
-Implicit Arguments Zp1 [[p']].
-Implicit Arguments inZp [[p']].
+Arguments Zp0 {p'}.
+Arguments Zp1 {p'}.
+Arguments inZp {p'}.
 
 Lemma ord1 : all_equal_to (0 : 'I_1).
 Proof. by case=> [[] // ?]; apply: val_inj. Qed.