diff options
65 files changed, 693 insertions, 694 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. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 6408b0b..ad0fa32 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -390,7 +390,7 @@ Qed. End StandardRepresentation. -Implicit Arguments grepr0 [R gT G]. +Arguments grepr0 [R gT G]. Prenex Implicits grepr0 dadd_grepr. Section Char. @@ -818,7 +818,7 @@ End IrrClass. Arguments Scope cfReg [_ group_scope]. Prenex Implicits cfIirr. -Implicit Arguments irr_inj [[gT] [G] x1 x2]. +Arguments irr_inj {gT G} [x1 x2]. Section IsChar. @@ -924,7 +924,7 @@ Canonical char_semiringPred := SemiringPred mul_char. End IsChar. Prenex Implicits character. -Implicit Arguments char_reprP [gT G phi]. +Arguments char_reprP [gT G phi]. Section AutChar. @@ -1870,7 +1870,7 @@ Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed. End Isom. -Implicit Arguments isom_Iirr_inj [aT rT G f R x1 x2]. +Arguments isom_Iirr_inj [aT rT G f R] isoGR [x1 x2]. Section IsomInv. @@ -1938,7 +1938,7 @@ Qed. End Sdprod. -Implicit Arguments sdprod_Iirr_inj [gT K H G x1 x2]. +Arguments sdprod_Iirr_inj [gT K H G] defG [x1 x2]. Section DProd. @@ -2089,7 +2089,7 @@ Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed. End DProd. -Implicit Arguments dprod_Iirr_inj [gT G K H x1 x2]. +Arguments dprod_Iirr_inj [gT G K H] KxH [x1 x2]. Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT}) (KxH : K \x H = G) (HxK : H \x K = G) i j : @@ -2257,7 +2257,7 @@ Qed. End Aut. -Implicit Arguments aut_Iirr_inj [gT G x1 x2]. +Arguments aut_Iirr_inj [gT G] u [x1 x2]. Section Coset. @@ -2554,7 +2554,7 @@ Qed. End DerivedGroup. -Implicit Arguments irr_prime_injP [gT G i]. +Arguments irr_prime_injP [gT G i]. (* Determinant characters and determinential order. *) Section DetOrder. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 81c26ab..3afaa82 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -557,7 +557,7 @@ rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq. rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_]. by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed. -Implicit Arguments cfun_onP [A phi]. +Arguments cfun_onP [A phi]. Lemma cfun_on0 A phi x : phi \in 'CF(G, A) -> x \notin A -> phi x = 0. Proof. by move/cfun_onP; apply. Qed. @@ -759,7 +759,7 @@ End ClassFun. Arguments Scope classfun_on [_ group_scope group_scope]. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. -Implicit Arguments cfun_onP [gT G A phi]. +Arguments cfun_onP [gT G A phi]. Hint Resolve cfun_onT. Section DotProduct. @@ -1009,7 +1009,7 @@ Lemma orthoPl phi S : Proof. by rewrite [orthogonal _ S]andbT /=; apply: (iffP allP) => ophiS ? /ophiS/eqP. Qed. -Implicit Arguments orthoPl [phi S]. +Arguments orthoPl [phi S]. Lemma orthogonal_sym : symmetric (@orthogonal _ G). Proof. @@ -1242,12 +1242,12 @@ Qed. End DotProduct. -Implicit Arguments orthoP [gT G phi psi]. -Implicit Arguments orthoPl [gT G phi S]. -Implicit Arguments orthoPr [gT G S psi]. -Implicit Arguments orthogonalP [gT G R S]. -Implicit Arguments pairwise_orthogonalP [gT G S]. -Implicit Arguments orthonormalP [gT G S]. +Arguments orthoP [gT G phi psi]. +Arguments orthoPl [gT G phi S]. +Arguments orthoPr [gT G S psi]. +Arguments orthogonalP [gT G S R]. +Arguments pairwise_orthogonalP [gT G S]. +Arguments orthonormalP [gT G S]. Section CfunOrder. @@ -1273,7 +1273,7 @@ Proof. by apply/eqP; rewrite -dvdn_cforder. Qed. End CfunOrder. -Implicit Arguments dvdn_cforderP [gT G phi n]. +Arguments dvdn_cforderP [gT G phi n]. Section MorphOrder. @@ -1621,7 +1621,7 @@ Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed. End InvMorphism. -Implicit Arguments cfIsom_inj [aT rT G R f x1 x2]. +Arguments cfIsom_inj [aT rT G f R] isoGR [x1 x2]. Section Coset. @@ -2487,9 +2487,9 @@ Proof. by rewrite rmorphM /= cfAutDprodl cfAutDprodr. Qed. End FieldAutomorphism. -Implicit Arguments cfAutK [[gT] [G]]. -Implicit Arguments cfAutVK [[gT] [G]]. -Implicit Arguments cfAut_inj [gT G x1 x2]. +Arguments cfAutK u {gT G}. +Arguments cfAutVK u {gT G}. +Arguments cfAut_inj u [gT G x1 x2]. Definition conj_cfRes := cfAutRes conjC. Definition cfker_conjC := cfker_aut conjC. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 9ae289d..7d4a84c 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -569,7 +569,7 @@ End Inertia. Arguments Scope inertia [_ group_scope cfun_scope]. Arguments Scope cfclass [_ group_scope cfun_scope group_scope]. -Implicit Arguments conjg_Iirr_inj [gT H x1 x2]. +Arguments conjg_Iirr_inj [gT H] y [x1 x2]. Notation "''I[' phi ] " := (inertia phi) : group_scope. Notation "''I[' phi ] " := (inertia_group phi) : Group_scope. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 0c1d4c1..fbd4bc3 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -427,7 +427,7 @@ Qed. End OneRepresentation. -Implicit Arguments rkerP [gT G n rG x]. +Arguments rkerP [gT G n rG x]. Section Proper. @@ -819,8 +819,8 @@ Arguments Scope mx_repr [_ _ group_scope nat_scope _]. Arguments Scope group_ring [_ _ group_scope]. Arguments Scope regular_repr [_ _ group_scope]. -Implicit Arguments centgmxP [R gT G n rG f]. -Implicit Arguments rkerP [R gT G n rG x]. +Arguments centgmxP [R gT G n rG f]. +Arguments rkerP [R gT G n rG x]. Prenex Implicits gring_mxK. Section ChangeOfRing. @@ -933,7 +933,7 @@ by apply: (iffP subsetP) => modU x Gx; have:= modU x Gx; rewrite !inE ?Gx. Qed. End Stabilisers. -Implicit Arguments mxmoduleP [m U]. +Arguments mxmoduleP [m U]. Lemma rstabS m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, n)) : (U <= V)%MS -> rstab rG V \subset rstab rG U. @@ -1288,7 +1288,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> j; rewrite !row_mul rowK mul_vec_lin /= mul_vec_lin_row. by rewrite -!row_mul mulmxBr !mulmxA cGf ?enum_valP // subrr !linear0. Qed. -Implicit Arguments hom_mxP [m f W]. +Arguments hom_mxP [m f W]. Lemma hom_envelop_mxC m f (W : 'M_(m, n)) A : (W <= dom_hom_mx f -> A \in E_G -> W *m A *m f = W *m f *m A)%MS. @@ -1366,7 +1366,7 @@ apply/sub_kermxP; rewrite mul_rV_lin1 /=; apply: (canLR vec_mxK). apply/row_matrixP=> i; rewrite row_mul rowK mul_vec_lin_row -row_mul. by rewrite mulmxBr mulmx1 cHW ?enum_valP // subrr !linear0. Qed. -Implicit Arguments rfix_mxP [m W]. +Arguments rfix_mxP [m W]. Lemma rfix_mx_id (H : {set gT}) x : x \in H -> rfix_mx H *m rG x = rfix_mx H. Proof. exact/rfix_mxP. Qed. @@ -1428,7 +1428,7 @@ rewrite genmxE; apply: (iffP submxP) => [[a] | [A /submxP[a defA]]] -> {v}. by rewrite vec_mxK submxMl. by exists a; rewrite mulmxA mul_rV_lin1 /= -defA mxvecK. Qed. -Implicit Arguments cyclic_mxP [u v]. +Arguments cyclic_mxP [u v]. Lemma cyclic_mx_id u : (u <= cyclic_mx u)%MS. Proof. by apply/cyclic_mxP; exists 1%:M; rewrite ?mulmx1 ?envelop_mx1. Qed. @@ -2366,19 +2366,19 @@ Qed. End OneRepresentation. -Implicit Arguments mxmoduleP [gT G n rG m U]. -Implicit Arguments envelop_mxP [gT G n rG A]. -Implicit Arguments hom_mxP [gT G n rG m f W]. -Implicit Arguments rfix_mxP [gT G n rG m W]. -Implicit Arguments cyclic_mxP [gT G n rG u v]. -Implicit Arguments annihilator_mxP [gT G n rG u A]. -Implicit Arguments row_hom_mxP [gT G n rG u v]. -Implicit Arguments mxsimple_isoP [gT G n rG U V]. -Implicit Arguments socleP [gT G n rG sG0 W W']. -Implicit Arguments mx_abs_irrP [gT G n rG]. +Arguments mxmoduleP [gT G n rG m U]. +Arguments envelop_mxP [gT G n rG A]. +Arguments hom_mxP [gT G n rG m f W]. +Arguments rfix_mxP [gT G n rG m W]. +Arguments cyclic_mxP [gT G n rG u v]. +Arguments annihilator_mxP [gT G n rG u A]. +Arguments row_hom_mxP [gT G n rG u v]. +Arguments mxsimple_isoP [gT G n rG U V]. +Arguments socleP [gT G n rG sG0 W W']. +Arguments mx_abs_irrP [gT G n rG]. -Implicit Arguments val_submod_inj [n U m]. -Implicit Arguments val_factmod_inj [n U m]. +Arguments val_submod_inj [n U m]. +Arguments val_factmod_inj [n U m]. Prenex Implicits val_submod_inj val_factmod_inj. @@ -4659,22 +4659,22 @@ Arguments Scope gset_mx [_ _ group_scope group_scope]. Arguments Scope classg_base [_ _ group_scope group_scope]. Arguments Scope irrType [_ _ group_scope group_scope]. -Implicit Arguments mxmoduleP [F gT G n rG m U]. -Implicit Arguments envelop_mxP [F gT G n rG A]. -Implicit Arguments hom_mxP [F gT G n rG m f W]. -Implicit Arguments mx_Maschke [F gT G n U]. -Implicit Arguments rfix_mxP [F gT G n rG m W]. -Implicit Arguments cyclic_mxP [F gT G n rG u v]. -Implicit Arguments annihilator_mxP [F gT G n rG u A]. -Implicit Arguments row_hom_mxP [F gT G n rG u v]. -Implicit Arguments mxsimple_isoP [F gT G n rG U V]. -Implicit Arguments socle_exists [F gT G n]. -Implicit Arguments socleP [F gT G n rG sG0 W W']. -Implicit Arguments mx_abs_irrP [F gT G n rG]. -Implicit Arguments socle_rsimP [F gT G n rG sG W1 W2]. - -Implicit Arguments val_submod_inj [F n U m]. -Implicit Arguments val_factmod_inj [F n U m]. +Arguments mxmoduleP [F gT G n rG m U]. +Arguments envelop_mxP [F gT G n rG A]. +Arguments hom_mxP [F gT G n rG m f W]. +Arguments mx_Maschke [F gT G n] rG _ [U]. +Arguments rfix_mxP [F gT G n rG m W]. +Arguments cyclic_mxP [F gT G n rG u v]. +Arguments annihilator_mxP [F gT G n rG u A]. +Arguments row_hom_mxP [F gT G n rG u v]. +Arguments mxsimple_isoP [F gT G n rG U V]. +Arguments socle_exists [F gT G n]. +Arguments socleP [F gT G n rG sG0 W W']. +Arguments mx_abs_irrP [F gT G n rG]. +Arguments socle_rsimP [F gT G n rG sG W1 W2]. + +Arguments val_submod_inj [F n U m]. +Arguments val_factmod_inj [F n U m]. Prenex Implicits val_submod_inj val_factmod_inj. Notation "'Cl" := (Clifford_action _) : action_scope. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 97ad828..5c9ca9b 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -709,7 +709,7 @@ End MoreVchar. Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class := [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)]. -Implicit Arguments dirr [[gT]]. +Arguments dirr {gT}. Section Norm1vchar. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 891bce5..3696316 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -260,7 +260,7 @@ Qed. Prenex Implicits alg_integral. Import DefaultKeying GRing.DefaultPred. -Implicit Arguments map_poly_inj [[F] [R] x1 x2]. +Arguments map_poly_inj {F R} f [x1 x2]. Theorem Fundamental_Theorem_of_Algebraics : {L : closedFieldType & diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v index 95d28cb..a6d11b3 100644 --- a/mathcomp/field/countalg.v +++ b/mathcomp/field/countalg.v @@ -59,7 +59,7 @@ Definition gen_pack T := End Generic. -Implicit Arguments gen_pack [type base_type class_of base_of base_sort]. +Arguments gen_pack [type base_type class_of base_of base_sort]. Local Notation cnt_ c := (@Countable.Class _ c c). Local Notation do_pack pack T := (pack T _ _ id _ _ _ id). Import GRing.Theory. diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 995dbee..e0ae1b1 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -641,12 +641,12 @@ Notation "[ 'aspace' 'of' U ]" := (@clone_aspace _ _ U _ _ id) Notation "[ 'aspace' 'of' U 'for' A ]" := (@clone_aspace _ _ U A _ idfun) (at level 0, format "[ 'aspace' 'of' U 'for' A ]") : form_scope. -Implicit Arguments prodvP [K aT U V W]. -Implicit Arguments cent1vP [K aT u v]. -Implicit Arguments centvP [K aT u V]. -Implicit Arguments centvsP [K aT U V]. -Implicit Arguments has_algidP [K aT U]. -Implicit Arguments polyOver1P [K aT p]. +Arguments prodvP [K aT U V W]. +Arguments cent1vP [K aT u v]. +Arguments centvP [K aT u V]. +Arguments centvsP [K aT U V]. +Arguments has_algidP [K aT U]. +Arguments polyOver1P [K aT p]. Section AspaceTheory. @@ -856,8 +856,8 @@ Notation "'C [ u ]" := (centraliser1_aspace u) : aspace_scope. Notation "'C ( V )" := (centraliser_aspace V) : aspace_scope. Notation "'Z ( A )" := (center_aspace A) : aspace_scope. -Implicit Arguments adim1P [K aT A]. -Implicit Arguments memv_cosetP [K aT U v w]. +Arguments adim1P [K aT A]. +Arguments memv_cosetP [K aT U v w]. Section Closure. @@ -1117,9 +1117,9 @@ Canonical linfun_ahom f := AHom (linfun_is_ahom f). End Class_Def. -Implicit Arguments ahom_in [aT rT]. -Implicit Arguments ahom_inP [aT rT f U]. -Implicit Arguments ahomP [aT rT f]. +Arguments ahom_in [aT rT]. +Arguments ahom_inP [aT rT f U]. +Arguments ahomP [aT rT f]. Section LRMorphism. @@ -1196,7 +1196,7 @@ Canonical fixedSpace_aspace aT (f : ahom aT aT) := [aspace of fixedSpace f]. End AHom. -Implicit Arguments ahom_in [K aT rT]. +Arguments ahom_in [K aT rT]. Notation "''AHom' ( aT , rT )" := (ahom aT rT) : type_scope. Notation "''AEnd' ( aT )" := (ahom aT aT) : type_scope. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 8d2af81..2a905e9 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -696,7 +696,7 @@ move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly. by apply: (polyOverSv sKE); rewrite minPolyOver. Qed. -Implicit Arguments Fadjoin_polyP [K x v]. +Arguments Fadjoin_polyP [K x v]. Lemma Fadjoin1_polyP x v : reflect (exists p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS). Proof. @@ -737,13 +737,13 @@ Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V)) Notation "E * F" := (prodv_aspace E F) : aspace_scope. Notation "f @: E" := (aimg_aspace f E) : aspace_scope. -Implicit Arguments Fadjoin_idP [F0 L K x]. -Implicit Arguments FadjoinP [F0 L K x E]. -Implicit Arguments Fadjoin_seqP [F0 L K rs E]. -Implicit Arguments polyOver_subvs [F0 L K p]. -Implicit Arguments Fadjoin_polyP [F0 L K x v]. -Implicit Arguments Fadjoin1_polyP [F0 L x v]. -Implicit Arguments minPoly_XsubC [F0 L K x]. +Arguments Fadjoin_idP [F0 L K x]. +Arguments FadjoinP [F0 L K x E]. +Arguments Fadjoin_seqP [F0 L K rs E]. +Arguments polyOver_subvs [F0 L K p]. +Arguments Fadjoin_polyP [F0 L K x v]. +Arguments Fadjoin1_polyP [F0 L x v]. +Arguments minPoly_XsubC [F0 L K x]. Section MapMinPoly. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index eaf5709..7e2fa17 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -329,9 +329,9 @@ End kHom. Notation "f ^-1" := (inv_ahom f) : lrfun_scope. -Implicit Arguments kHomP [F L K V f]. -Implicit Arguments kAHomP [F L U V f]. -Implicit Arguments kHom_lrmorphism [F L f]. +Arguments kHomP [F L K V f]. +Arguments kAHomP [F L U V f]. +Arguments kHom_lrmorphism [F L f]. Module SplittingField. @@ -1205,7 +1205,7 @@ have [x galEx Df] := kHom_to_gal sK_Ka_E nKE homKa_f; exists x => //. by rewrite -Df ?memv_adjoin // (kHomExtend_val (kHom1 K K)) ?lfun1_poly. Qed. -Implicit Arguments normalFieldP [K E]. +Arguments normalFieldP [K E]. Lemma normalField_factors K E : (K <= E)%VS -> @@ -1637,7 +1637,7 @@ End GaloisTheory. Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope. Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope. -Implicit Arguments fixedFieldP [F L E A a]. -Implicit Arguments normalFieldP [F L K E]. -Implicit Arguments splitting_galoisField [F L K E]. -Implicit Arguments galois_fixedField [F L K E]. +Arguments fixedFieldP [F L E A a]. +Arguments normalFieldP [F L K E]. +Arguments splitting_galoisField [F L K E]. +Arguments galois_fixedField [F L K E]. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index c3f3ebb..c5a1118 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -170,7 +170,7 @@ Qed. End SeparablePoly. -Implicit Arguments separable_polyP [R p]. +Arguments separable_polyP [R p]. Lemma separable_map (F : fieldType) (R : idomainType) (f : {rmorphism F -> R}) (p : {poly F}) : @@ -544,7 +544,7 @@ Qed. End SeparableElement. -Implicit Arguments separable_elementP [K x]. +Arguments separable_elementP [K x]. Lemma separable_elementS K E x : (K <= E)%VS -> separable_element K x -> separable_element E x. @@ -992,10 +992,10 @@ Qed. End Separable. -Implicit Arguments separable_elementP [F L K x]. -Implicit Arguments separablePn [F L K x]. -Implicit Arguments Derivation_separableP [F L K x]. -Implicit Arguments adjoin_separableP [F L K x]. -Implicit Arguments purely_inseparable_elementP [F L K x]. -Implicit Arguments separableP [F L K E]. -Implicit Arguments purely_inseparableP [F L K E]. +Arguments separable_elementP [F L K x]. +Arguments separablePn [F L K x]. +Arguments Derivation_separableP [F L K x]. +Arguments adjoin_separableP [F L K x]. +Arguments purely_inseparable_elementP [F L K x]. +Arguments separableP [F L K E]. +Arguments purely_inseparableP [F L K E]. diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index ecfa6ea..6478c81 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -287,7 +287,7 @@ Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT). Implicit Types (a : aT) (x y : rT) (A B : {set aT}) (S T : {set rT}). Lemma act_inj : left_injective to. Proof. by case: to => ? []. Qed. -Implicit Arguments act_inj []. +Arguments act_inj : clear implicits. Lemma actMin x : {in D &, act_morph to x}. Proof. by case: to => ? []. Qed. @@ -486,17 +486,17 @@ End RawAction. (* Warning: this directive depends on names of bound variables in the *) (* definition of injective, in ssrfun.v. *) -Implicit Arguments act_inj [[aT] [D] [rT] x1 x2]. +Arguments act_inj {aT D rT} to _ [x1 x2]. Notation "to ^*" := (set_action to) : action_scope. -Implicit Arguments orbitP [aT D rT to A x y]. -Implicit Arguments afixP [aT D rT to A x]. -Implicit Arguments afix1P [aT D rT to a x]. +Arguments orbitP [aT D rT to A x y]. +Arguments afixP [aT D rT to A x]. +Arguments afix1P [aT D rT to a x]. Prenex Implicits orbitP afixP afix1P. -Implicit Arguments reindex_astabs [aT D rT vT idx op S F]. -Implicit Arguments reindex_acts [aT D rT vT idx op S A a F]. +Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F]. +Arguments reindex_acts [aT D rT] to [vT idx op S A a F]. Section PartialAction. (* Lemmas that require a (partial) group domain. *) @@ -879,9 +879,9 @@ End PartialAction. Arguments Scope orbit_transversal [_ group_scope _ action_scope group_scope group_scope]. -Implicit Arguments orbit_in_eqP [aT D rT to G x y]. -Implicit Arguments orbit1P [aT D rT to G x]. -Implicit Arguments contra_orbit [aT D rT x y]. +Arguments orbit_in_eqP [aT D rT to G x y]. +Arguments orbit1P [aT D rT to G x]. +Arguments contra_orbit [aT D rT] to G [x y]. Prenex Implicits orbit_in_eqP orbit1P. Notation "''C' ( S | to )" := (astab_group to S) : Group_scope. @@ -1008,7 +1008,7 @@ Proof. apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act. by apply/subsetP=> a Aa; rewrite !inE; apply/subsetP=> x; rewrite inE nSA. Qed. -Implicit Arguments actsP [A S]. +Arguments actsP [A S]. Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b). Proof. @@ -1137,13 +1137,13 @@ Qed. End TotalActions. -Implicit Arguments astabP [aT rT to S a]. -Implicit Arguments orbit_eqP [aT rT to G x y]. -Implicit Arguments astab1P [aT rT to x a]. -Implicit Arguments astabsP [aT rT to S a]. -Implicit Arguments atransP [aT rT to G S]. -Implicit Arguments actsP [aT rT to A S]. -Implicit Arguments faithfulP [aT rT to A S]. +Arguments astabP [aT rT to S a]. +Arguments orbit_eqP [aT rT to G x y]. +Arguments astab1P [aT rT to x a]. +Arguments astabsP [aT rT to S a]. +Arguments atransP [aT rT to G S]. +Arguments actsP [aT rT to A S]. +Arguments faithfulP [aT rT to A S]. Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP. Section Restrict. @@ -1637,7 +1637,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed. End PermAction. -Implicit Arguments perm_act1P [rT a]. +Arguments perm_act1P [rT a]. Prenex Implicits perm_act1P. Notation "'P" := (perm_action _) (at level 8) : action_scope. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 8813b45..e727aba 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -198,7 +198,7 @@ Qed. End MakeAut. -Implicit Arguments morphim_fixP [gT G f]. +Arguments morphim_fixP [gT G f]. Prenex Implicits aut morphim_fixP. Section AutIsom. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index dd57af4..5afc3c7 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -493,7 +493,7 @@ Qed. End PreGroupIdentities. Hint Resolve commute1. -Implicit Arguments invg_inj [T]. +Arguments invg_inj [T]. Prenex Implicits commute invgK invg_inj. Section GroupIdentities. @@ -641,11 +641,11 @@ Ltac gsimpl := autorewrite with gsimpl; try done. Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)). Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))). -Implicit Arguments mulgI [T]. -Implicit Arguments mulIg [T]. -Implicit Arguments conjg_inj [T]. -Implicit Arguments commgP [T x y]. -Implicit Arguments conjg_fixP [T x y]. +Arguments mulgI [T]. +Arguments mulIg [T]. +Arguments conjg_inj [T]. +Arguments commgP [T x y]. +Arguments conjg_fixP [T x y]. Prenex Implicits conjg_fixP commgP. Section Repr. @@ -672,7 +672,7 @@ Proof. by rewrite /repr; case: pickP => [x|_]; rewrite !inE. Qed. End Repr. -Implicit Arguments mem_repr [gT A]. +Arguments mem_repr [gT A]. Section BaseSetMulDef. (* We only assume a baseFinGroupType to allow this construct to be iterated. *) @@ -946,9 +946,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed. End BaseSetMulProp. -Implicit Arguments set1gP [gT x]. -Implicit Arguments mulsgP [gT A B x]. -Implicit Arguments prodsgP [gT I P A x]. +Arguments set1gP [gT x]. +Arguments mulsgP [gT A B x]. +Arguments prodsgP [gT I P A x]. Section GroupSetMulProp. (* Constructs that need a finGroupType *) @@ -1304,11 +1304,11 @@ Definition order x := #|cycle x|. End GroupSetMulProp. -Implicit Arguments lcosetP [gT A x y]. -Implicit Arguments lcosetsP [gT A B C]. -Implicit Arguments rcosetP [gT A x y]. -Implicit Arguments rcosetsP [gT A B C]. -Implicit Arguments group_setP [gT A]. +Arguments lcosetP [gT A x y]. +Arguments lcosetsP [gT A B C]. +Arguments rcosetP [gT A x y]. +Arguments rcosetsP [gT A B C]. +Arguments group_setP [gT A]. Prenex Implicits group_set mulsgP set1gP. Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP. @@ -1858,15 +1858,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope. Prenex Implicits subg sgval subg_of. Bind Scope group_scope with subg_of. -Implicit Arguments trivgP [gT G]. -Implicit Arguments trivGP [gT G]. -Implicit Arguments lcoset_eqP [gT G x y]. -Implicit Arguments rcoset_eqP [gT G x y]. -Implicit Arguments mulGidPl [gT G H]. -Implicit Arguments mulGidPr [gT G H]. -Implicit Arguments comm_group_setP [gT G H]. -Implicit Arguments class_eqP [gT G x y]. -Implicit Arguments repr_classesP [gT G xG]. +Arguments trivgP [gT G]. +Arguments trivGP [gT G]. +Arguments lcoset_eqP [gT G x y]. +Arguments rcoset_eqP [gT G x y]. +Arguments mulGidPl [gT G H]. +Arguments mulGidPr [gT G H]. +Arguments comm_group_setP [gT G H]. +Arguments class_eqP [gT G x y]. +Arguments repr_classesP [gT G xG]. Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP. Section GroupInter. @@ -2396,11 +2396,11 @@ Qed. End GeneratedGroup. -Implicit Arguments gen_prodgP [gT A x]. -Implicit Arguments joing_idPl [gT G A]. -Implicit Arguments joing_idPr [gT A G]. -Implicit Arguments mulGsubP [gT K H G]. -Implicit Arguments joing_subP [gT A B G]. +Arguments gen_prodgP [gT A x]. +Arguments joing_idPl [gT G A]. +Arguments joing_idPr [gT A G]. +Arguments mulGsubP [gT K H G]. +Arguments joing_subP [gT A B G]. Section Cycles. @@ -2524,7 +2524,7 @@ Proof. suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed. -Implicit Arguments normP [x A]. +Arguments normP [x A]. Lemma group_set_normaliser A : group_set 'N(A). Proof. @@ -2539,7 +2539,7 @@ Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. by apply/normP; apply: nBA. Qed. -Implicit Arguments normsP [A B]. +Arguments normsP [A B]. Lemma memJ_norm x y A : x \in 'N(A) -> (y ^ x \in A) = (y \in A). Proof. by move=> Nx; rewrite -{1}(normP Nx) memJ_conjg. Qed. @@ -2987,13 +2987,13 @@ End SubAbelian. End Normaliser. -Implicit Arguments normP [gT x A]. -Implicit Arguments centP [gT x A]. -Implicit Arguments normsP [gT A B]. -Implicit Arguments cent1P [gT x y]. -Implicit Arguments normalP [gT A B]. -Implicit Arguments centsP [gT A B]. -Implicit Arguments commG1P [gT A B]. +Arguments normP [gT x A]. +Arguments centP [gT A x]. +Arguments normsP [gT A B]. +Arguments cent1P [gT x y]. +Arguments normalP [gT A B]. +Arguments centsP [gT A B]. +Arguments commG1P [gT A B]. Prenex Implicits normP normsP cent1P normalP centP centsP commG1P. @@ -3091,6 +3091,6 @@ Notation "[ 'min' A 'of' G | gP & gQ ]" := [min A of G | gP && gQ] : group_scope. Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope. -Implicit Arguments mingroupP [gT gP G]. -Implicit Arguments maxgroupP [gT gP G]. +Arguments mingroupP [gT gP G]. +Arguments maxgroupP [gT gP G]. Prenex Implicits mingroupP maxgroupP. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index cd129f2..dc16021 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -96,10 +96,10 @@ Arguments Scope complements_to_in [_ group_scope group_scope]. Arguments Scope splits_over [_ group_scope group_scope]. Arguments Scope remgr [_ group_scope group_scope group_scope]. Arguments Scope divgr [_ group_scope group_scope group_scope]. -Implicit Arguments partial_product []. -Implicit Arguments semidirect_product []. -Implicit Arguments central_product []. -Implicit Arguments direct_product []. +Arguments partial_product : clear implicits. +Arguments semidirect_product : clear implicits. +Arguments central_product : clear implicits. +Arguments direct_product : clear implicits. Notation pprod := (partial_product _). Notation sdprod := (semidirect_product _). Notation cprod := (central_product _). @@ -870,11 +870,11 @@ Qed. End InternalProd. -Implicit Arguments complP [gT H A B]. -Implicit Arguments splitsP [gT A B]. -Implicit Arguments sdprod_normal_complP [gT K H G]. -Implicit Arguments dprodYP [gT K H]. -Implicit Arguments bigdprodYP [gT I P F]. +Arguments complP [gT H A B]. +Arguments splitsP [gT B A]. +Arguments sdprod_normal_complP [gT G K H]. +Arguments dprodYP [gT K H]. +Arguments bigdprodYP [gT I P F]. Section MorphimInternalProd. @@ -1703,5 +1703,5 @@ Qed. End DirprodIsom. -Implicit Arguments mulgmP [gT H1 H2 G]. +Arguments mulgmP [gT H1 H2 G]. Prenex Implicits mulgm mulgmP. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 2a70706..315358b 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -118,8 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" := Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f)) (at level 0, format "[ 'morphism' 'of' f ]") : form_scope. -Implicit Arguments morphimP [aT rT D A f y]. -Implicit Arguments morphpreP [aT rT D R f x]. +Arguments morphimP [aT rT D A y f]. +Arguments morphpreP [aT rT D R x f]. Prenex Implicits morphimP morphpreP. (* Domain, image, preimage, kernel, using phantom types to infer the domain. *) @@ -873,7 +873,7 @@ Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope. Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope. Notation "f @: D" := (morph_dom_group f D) : Group_scope. -Implicit Arguments injmP [aT rT D f]. +Arguments injmP [aT rT D f]. Section IdentityMorphism. @@ -969,8 +969,8 @@ End RestrictedMorphism. Arguments Scope restrm [_ _ group_scope group_scope _ group_scope]. Prenex Implicits restrm. -Implicit Arguments restrmP [aT rT D A]. -Implicit Arguments domP [aT rT D A]. +Arguments restrmP [aT rT A D]. +Arguments domP [aT rT A D]. Section TrivMorphism. @@ -995,7 +995,7 @@ Proof. by apply/setIidPl/subsetP=> x _; rewrite !inE /=. Qed. End TrivMorphism. Arguments Scope trivm [_ _ group_scope group_scope]. -Implicit Arguments trivm [[aT] [rT]]. +Arguments trivm {aT rT}. (* The composition of two morphisms is a Canonical morphism instance. *) Section MorphismComposition. @@ -1259,7 +1259,7 @@ End Defs. Infix "\isog" := isog. -Implicit Arguments isom_isog [A B D]. +Arguments isom_isog [A B D]. (* The real reflection properties only hold for true groups and morphisms. *) @@ -1330,11 +1330,11 @@ Arguments Scope morphic [_ _ group_scope _]. Arguments Scope misom [_ _ group_scope group_scope _]. Arguments Scope isog [_ _ group_scope group_scope]. -Implicit Arguments morphicP [aT rT A f]. -Implicit Arguments misomP [aT rT A B f]. -Implicit Arguments isom_isog [aT rT A B D]. -Implicit Arguments isomP [aT rT G H f]. -Implicit Arguments isogP [aT rT G H]. +Arguments morphicP [aT rT A f]. +Arguments misomP [aT rT A B f]. +Arguments isom_isog [aT rT A B D]. +Arguments isomP [aT rT G H f]. +Arguments isogP [aT rT G H]. Prenex Implicits morphic morphicP morphm isom isog isomP misomP isogP. Notation "x \isog y":= (isog x y). @@ -1483,7 +1483,7 @@ Arguments Scope homg [_ _ group_scope group_scope]. Notation "G \homg H" := (homg G H) (at level 70, no associativity) : group_scope. -Implicit Arguments homgP [rT aT C D]. +Arguments homgP [rT aT C D]. (* Isomorphism between a group and its subtype. *) diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 6d9abdc..bbf4363 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -128,7 +128,7 @@ Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. Lemma perm_inj s : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. -Implicit Arguments perm_inj []. +Arguments perm_inj : clear implicits. Hint Resolve perm_inj. Lemma perm_onto s : codom s =i predT. @@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed. Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT]. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. @@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed. End PermutationParity. Coercion odd_perm : perm_type >-> bool. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 242b4b7..99d1aef 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -751,8 +751,8 @@ Qed. End EqIso. -Implicit Arguments qisom_inj [gT G H]. -Implicit Arguments morphim_qisom_inj [gT G H]. +Arguments qisom_inj [gT G H]. +Arguments morphim_qisom_inj [gT G H]. Section FirstIsomorphism. diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v index 7cc32ed..ea39e9d 100644 --- a/mathcomp/odd_order/BGsection12.v +++ b/mathcomp/odd_order/BGsection12.v @@ -241,9 +241,9 @@ Qed. End Introduction. -Implicit Arguments tau2'1 [[M] x]. -Implicit Arguments tau3'1 [[M] x]. -Implicit Arguments tau3'2 [[M] x]. +Arguments tau2'1 {M} [x]. +Arguments tau3'1 {M} [x]. +Arguments tau3'2 {M} [x]. (* This is the rest of B & G, Lemma 12.1 (parts b, c, d,e, and f). *) Lemma sigma_compl_context M E E1 E2 E3 : @@ -2680,7 +2680,7 @@ Qed. End Section12. -Implicit Arguments tau2'1 [[gT] [M] x]. -Implicit Arguments tau3'1 [[gT] [M] x]. -Implicit Arguments tau3'2 [[gT] [M] x]. +Arguments tau2'1 {gT M} [x]. +Arguments tau3'1 {gT M} [x]. +Arguments tau3'2 {gT M} [x]. diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v index 5f803b0..08a589e 100644 --- a/mathcomp/odd_order/BGsection7.v +++ b/mathcomp/odd_order/BGsection7.v @@ -267,7 +267,7 @@ Proof. by rewrite inE mmaxJ conjSg !inE. Qed. Lemma uniq_mmaxP U : reflect (exists M, 'M(U) = [set M]) (U \in 'U). Proof. by rewrite inE; apply: cards1P. Qed. -Implicit Arguments uniq_mmaxP [U]. +Arguments uniq_mmaxP [U]. Lemma mem_uniq_mmax U M : 'M(U) = [set M] -> M \in 'M /\ U \subset M. Proof. by move/setP/(_ M); rewrite set11 => /setIdP. Qed. @@ -354,7 +354,7 @@ Qed. End MinSimpleOdd. -Implicit Arguments uniq_mmaxP [gT U]. +Arguments uniq_mmaxP [gT U]. Prenex Implicits uniq_mmaxP. Notation "''M'" := (minSimple_max_groups _) : group_scope. diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index 6bff279..3c62a9e 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.v @@ -260,7 +260,7 @@ suffices ->: sub_bbox (th_bbox th) bb = all in_bb th by apply: allP. elim: th => [|[[i j] _] th] //=; case: (th_bbox th) => ri rj /=. by rewrite /sub_bbox /= !geq_max andbACA => ->. Qed. -Implicit Arguments th_bboxP [th bb]. +Arguments th_bboxP [th bb]. Fixpoint th_dim th : nat := if th is (_, kvs) :: th1 then @@ -277,7 +277,7 @@ suffices ->: (th_dim th <= bk)%N = all in_bk th. elim: th => // [[_ kvs] th /= <-]; elim: kvs => //= kv kvs. by rewrite -andbA geq_max => ->. Qed. -Implicit Arguments th_dimP [th bk]. +Arguments th_dimP [th bk]. (* Theory and clause lookup. *) @@ -468,7 +468,7 @@ split; first by apply/th_bboxP=> cl /thP[]. by apply/th_dimP=> cl /thP[_ _ clP] kv /clP[]. by apply/allP=> cl /thP[_ Ucl clP]; rewrite /sat_cl Ucl; apply/allP=> kv /clP[]. Qed. -Implicit Arguments satP [m th]. +Arguments satP [m th]. (* Reflexion of the dot product. *) @@ -573,7 +573,7 @@ suffices{Dthx} m_th1: sat m th1. apply/satP=> cl1; rewrite Dth1 inE; case: ifP => [_ /eqP-> | _ /thP] //=. by rewrite cl'k; split=> // kv /predU1P[-> | /clP//]; rewrite /sat_lit Dv. Qed. -Implicit Arguments sat_cases [m th cl]. +Arguments sat_cases [m th] k [cl]. Definition unsat_cases_hyp th0 kvs tO cl := let: (k, _) := head (2, 0) kvs in let thk_ := ext_cl th0 cl k in @@ -797,14 +797,14 @@ Proof. by case: find_sym => // s; apply: unsat_match. Qed. End Interpretation. -Implicit Arguments satP [gT G m th]. -Implicit Arguments unsat [gT G]. -Implicit Arguments sat_cases [gT G m th cl]. -Implicit Arguments unsat_cases [gT G th tO]. -Implicit Arguments unsat_wlog [gT G]. -Implicit Arguments unsat_fill [gT G]. -Implicit Arguments unsat_consider [gT G]. -Implicit Arguments unsat_match [gT G th1 th2]. +Arguments satP [gT G m th]. +Arguments unsat [gT G]. +Arguments sat_cases [gT G m th] k [cl]. +Arguments unsat_cases [gT G th] ij kvs [tO]. +Arguments unsat_wlog [gT G]. +Arguments unsat_fill [gT G]. +Arguments unsat_consider [gT G]. +Arguments unsat_match [gT G] s [th1 th2]. (* The domain-specific tactic language. *) @@ -1829,7 +1829,7 @@ End AutCyclicTI. End Three. -Implicit Arguments ortho_cycTIiso_vanish [gT G W W1 W2 defW psi]. +Arguments ortho_cycTIiso_vanish [gT G W W1 W2 defW] ctiW [psi]. Section ThreeSymmetry. diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v index b5f9344..2be2adb 100644 --- a/mathcomp/odd_order/PFsection4.v +++ b/mathcomp/odd_order/PFsection4.v @@ -692,10 +692,10 @@ Notation primeTIsign ptiW j := Notation primeTIirr ptiW i j := 'chi_(primeTI_Iirr ptiW (i, j)) (only parsing). Notation primeTIres ptiW j := 'chi_(primeTI_Ires ptiW j) (only parsing). -Implicit Arguments prTIirr_inj [gT L K W W1 W2 defW x1 x2]. -Implicit Arguments prTIred_inj [gT L K W W1 W2 defW x1 x2]. -Implicit Arguments prTIres_inj [gT L K W W1 W2 defW x1 x2]. -Implicit Arguments not_prTIirr_vanish [gT L K W W1 W2 defW k]. +Arguments prTIirr_inj [gT L K W W1 W2 defW] ptiWL [x1 x2]. +Arguments prTIred_inj [gT L K W W1 W2 defW] ptiWL [x1 x2]. +Arguments prTIres_inj [gT L K W W1 W2 defW] ptiWL [x1 x2]. +Arguments not_prTIirr_vanish [gT L K W W1 W2 defW] ptiWL [k]. Section Four_6_t0_10. diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index e42e104..94e9c42 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.v @@ -263,7 +263,7 @@ End Beta. End SeqInd. -Implicit Arguments seqIndP [calX phi]. +Arguments seqIndP [calX phi]. Lemma seqIndS (calX calY : {set Iirr K}) : calX \subset calY -> {subset seqInd calX <= seqInd calY}. @@ -443,8 +443,8 @@ Proof. by rewrite sum_seqIndD_square ?normal1 ?sub1G // indexg1. Qed. End InducedIrrs. -Implicit Arguments seqIndP [gT K L calX phi]. -Implicit Arguments seqIndC1P [gT K L phi]. +Arguments seqIndP [gT K L calX phi]. +Arguments seqIndC1P [gT K L phi]. Section Five. @@ -1605,5 +1605,5 @@ End DadeAut. End Five. -Implicit Arguments coherent_prDade_TIred - [gT G H L K W W1 W2 A0 A S0 k tau1 defW].
\ No newline at end of file +Arguments coherent_prDade_TIred + [gT G H L K W W1 W2 S0 A A0 k tau1 defW].
\ No newline at end of file diff --git a/mathcomp/real_closed/mxtens.v b/mathcomp/real_closed/mxtens.v index 4e6b72a..792e223 100644 --- a/mathcomp/real_closed/mxtens.v +++ b/mathcomp/real_closed/mxtens.v @@ -44,8 +44,8 @@ Proof. by rewrite ltn_mod; case: n k=> //; rewrite muln0=> [] []. Qed. Definition mxtens_unindex m n k := (Ordinal (@mxtens_index_proof1 m n k), Ordinal (@mxtens_index_proof2 m n k)). -Implicit Arguments mxtens_index [[m] [n]]. -Implicit Arguments mxtens_unindex [[m] [n]]. +Arguments mxtens_index {m n}. +Arguments mxtens_unindex {m n}. Lemma mxtens_indexK m n : cancel (@mxtens_index m n) (@mxtens_unindex m n). Proof. diff --git a/mathcomp/real_closed/ordered_qelim.v b/mathcomp/real_closed/ordered_qelim.v index 4779540..5f4e7f5 100644 --- a/mathcomp/real_closed/ordered_qelim.v +++ b/mathcomp/real_closed/ordered_qelim.v @@ -76,7 +76,7 @@ Canonical term_eqMixin (T : eqType) := EqMixin (@term_eqP T). Canonical term_eqType (T : eqType) := Eval hnf in EqType (term T) (@term_eqMixin T). -Implicit Arguments term_eqP [x y]. +Arguments term_eqP T [x y]. Prenex Implicits term_eq. @@ -98,7 +98,7 @@ Arguments Scope Not [_ oterm_scope]. Arguments Scope Exists [_ nat_scope oterm_scope]. Arguments Scope Forall [_ nat_scope oterm_scope]. -Implicit Arguments Bool [T]. +Arguments Bool [T]. Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not. Prenex Implicits Exists Forall Lt. @@ -199,7 +199,7 @@ Canonical oclause_eqMixin (T : eqType) := EqMixin (@oclause_eqP T). Canonical oclause_eqType (T : eqType) := Eval hnf in EqType (oclause T) (@oclause_eqMixin T). -Implicit Arguments oclause_eqP [x y]. +Arguments oclause_eqP T [x y]. Prenex Implicits oclause_eq. Section EvalTerm. diff --git a/mathcomp/real_closed/qe_rcf.v b/mathcomp/real_closed/qe_rcf.v index 272c44a..c2e0333 100644 --- a/mathcomp/real_closed/qe_rcf.v +++ b/mathcomp/real_closed/qe_rcf.v @@ -114,7 +114,7 @@ Arguments Scope Or [_ qf_scope qf_scope]. Arguments Scope Implies [_ qf_scope qf_scope]. Arguments Scope Not [_ qf_scope]. -Implicit Arguments Bool [R]. +Arguments Bool [R]. Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt. Prenex Implicits to_rterm. @@ -537,7 +537,7 @@ rewrite lead_coefDl ?lead_coefMX ?size_mulX // ltnS size_polyC. by rewrite (leq_trans (leq_b1 _)) // size_poly_gt0. Qed. -Implicit Arguments eval_LeadCoef [e p k]. +Arguments eval_LeadCoef [e p k]. Prenex Implicits eval_LeadCoef. Lemma eval_AmulXn a n e : eval_poly e (AmulXn a n) = (eval e a)%:P * 'X^n. @@ -625,7 +625,7 @@ rewrite (ihps _ (fun ps => k' (eval e lp :: ps))) => //= lps. by rewrite Pk. Qed. -Implicit Arguments eval_SeqPInfty [e ps k]. +Arguments eval_SeqPInfty [e ps k]. Prenex Implicits eval_SeqPInfty. Lemma eval_SeqMInfty e ps k k' : @@ -640,7 +640,7 @@ rewrite eval_Size /= /k'' {k''}. by set X := map _ _; grab_eq k'' X; apply: ihps => {X} lps; rewrite Pk. Qed. -Implicit Arguments eval_SeqMInfty [e ps k]. +Arguments eval_SeqMInfty [e ps k]. Prenex Implicits eval_SeqMInfty. Lemma eval_ChangesPoly e ps k : qf_eval e (ChangesPoly ps k) = @@ -682,7 +682,7 @@ set X := lead_coef _; grab_eq k'' X; apply: eval_LeadCoef => {X}. by move=> x; rewrite ihn // !eval_OpPoly /= !mul_polyC. Qed. -Implicit Arguments eval_Rediv_rec_loop [e q sq cq c qq r n k]. +Arguments eval_Rediv_rec_loop [e q sq cq c qq r n k]. Prenex Implicits eval_Rediv_rec_loop. Lemma eval_Rediv e p q k k' (d := (redivp (eval_poly e p) (eval_poly e q))) : @@ -698,7 +698,7 @@ rewrite (eval_LeadCoef (fun lq => by rewrite redivp_rec_loopP. Qed. -Implicit Arguments eval_Rediv [e p q k]. +Arguments eval_Rediv [e p q k]. Prenex Implicits eval_Rediv. Lemma eval_NextMod e p q k k' : @@ -716,7 +716,7 @@ rewrite (eval_Rediv (fun mpq => by rewrite Pk !eval_OpPoly. Qed. -Implicit Arguments eval_NextMod [e p q k]. +Arguments eval_NextMod [e p q k]. Prenex Implicits eval_NextMod. Lemma eval_Rgcd_loop e n p q k k' : @@ -759,7 +759,7 @@ rewrite big_cons (ihsp _ (fun r => k' (rgcdp (eval_poly e p) r))) //. by move=> r; apply: eval_Rgcd. Qed. -Implicit Arguments eval_Rgcd [e p q k]. +Arguments eval_Rgcd [e p q k]. Prenex Implicits eval_Rgcd. @@ -781,7 +781,7 @@ rewrite (eval_NextMod (fun npq => k' (p' :: mods_aux q' npq n))) => // npq. by rewrite (ihn _ _ _ (fun ps => k' (p' :: ps))) => // ps; rewrite Pk. Qed. -Implicit Arguments eval_ModsAux [e p q n k]. +Arguments eval_ModsAux [e p q n k]. Prenex Implicits eval_ModsAux. Lemma eval_Mods e p q k k' : @@ -789,7 +789,7 @@ Lemma eval_Mods e p q k k' : qf_eval e (Mods p q k) = k' (mods (eval_poly e p) (eval_poly e q)). Proof. by move=> Pk; rewrite !eval_Size; apply: eval_ModsAux. Qed. -Implicit Arguments eval_Mods [e p q k]. +Arguments eval_Mods [e p q k]. Prenex Implicits eval_Mods. Lemma eval_TaqR e p q k : @@ -831,7 +831,7 @@ Lemma eval_TaqsR e p sq i k k' : k' (taqsR (eval_poly e p) (map (eval_poly e) sq) i). Proof. by move=> Pk; rewrite /TaqsR /taqsR eval_TaqR Pk /= eval_Pcq. Qed. -Implicit Arguments eval_TaqsR [e p sq i k]. +Arguments eval_TaqsR [e p sq i k]. Prenex Implicits eval_TaqsR. Fact invmx_ctmat1 : invmx (map_mx (intr : int -> F) ctmat1) = @@ -885,7 +885,7 @@ rewrite (eval_TaqsR by move=> y; rewrite (ihn _ k') // -(eval_Coefs e). Qed. -Implicit Arguments eval_CcountWeak [e p sq k]. +Arguments eval_CcountWeak [e p sq k]. Prenex Implicits eval_CcountWeak. Lemma eval_ProdPoly e T s f k f' k' : @@ -902,7 +902,7 @@ move=> fa; rewrite (ihs _ (fun fs => k' (eval_poly e fa * fs))) //. by move=> fs; rewrite Pk eval_OpPoly. Qed. -Implicit Arguments eval_ProdPoly [e T s f k]. +Arguments eval_ProdPoly [e T s f k]. Prenex Implicits eval_ProdPoly. Lemma eval_BoundingPoly e sq : diff --git a/mathcomp/real_closed/realalg.v b/mathcomp/real_closed/realalg.v index 0cbba9f..7d9d987 100644 --- a/mathcomp/real_closed/realalg.v +++ b/mathcomp/real_closed/realalg.v @@ -194,11 +194,11 @@ Definition eq_algcreal : rel algcreal := eq_algcreal_dec. Lemma eq_algcrealP (x y : algcreal) : reflect (x == y)%CR (eq_algcreal x y). Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed. -Implicit Arguments eq_algcrealP [x y]. +Arguments eq_algcrealP [x y]. Lemma neq_algcrealP (x y : algcreal) : reflect (x != y)%CR (~~ eq_algcreal x y). Proof. by rewrite /eq_algcreal; case: eq_algcreal_dec=> /=; constructor. Qed. -Implicit Arguments neq_algcrealP [x y]. +Arguments neq_algcrealP [x y]. Prenex Implicits eq_algcrealP neq_algcrealP. Fact eq_algcreal_is_equiv : equiv_class_of eq_algcreal. @@ -284,11 +284,11 @@ Definition le_algcreal : rel algcreal := fun x y => ~~ ltVge_algcreal_dec y x. Lemma lt_algcrealP (x y : algcreal) : reflect (x < y)%CR (lt_algcreal x y). Proof. by rewrite /lt_algcreal; case: ltVge_algcreal_dec; constructor. Qed. -Implicit Arguments lt_algcrealP [x y]. +Arguments lt_algcrealP [x y]. Lemma le_algcrealP (x y : algcreal) : reflect (x <= y)%CR (le_algcreal x y). Proof. by rewrite /le_algcreal; case: ltVge_algcreal_dec; constructor. Qed. -Implicit Arguments le_algcrealP [x y]. +Arguments le_algcrealP [x y]. Prenex Implicits lt_algcrealP le_algcrealP. Definition exp_algcreal x n := iterop n mul_algcreal x one_algcreal. @@ -609,7 +609,7 @@ Qed. Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod {alg F}]). Proof. by rewrite eqquotE; apply: neq_algcrealP. Qed. -Implicit Arguments nequiv_alg [x y]. +Arguments nequiv_alg [x y]. Prenex Implicits nequiv_alg. Lemma pi_algK (x : algcreal) : (repr (\pi_{alg F} x) == x)%CR. @@ -711,7 +711,7 @@ elim/quotW=> x; elim/quotW=> y; elim/quotW=> z; rewrite !piE -equiv_alg /=. by apply: eq_crealP; exists m0=> * /=; rewrite mulrDl subrr normr0. Qed. -Implicit Arguments neq_creal_cst [F x y]. +Arguments neq_creal_cst [F x y]. Prenex Implicits neq_creal_cst. Lemma nonzero1_alg : one_alg != zero_alg. @@ -964,11 +964,11 @@ Proof. by rewrite [`|_|]piE. Qed. Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_{alg F} x < \pi y). Proof. by rewrite lt_pi; apply: lt_algcrealP. Qed. -Implicit Arguments lt_algP [x y]. +Arguments lt_algP [x y]. Lemma le_algP (x y : algcreal) : reflect (x <= y)%CR (\pi_{alg F} x <= \pi y). Proof. by rewrite le_pi; apply: le_algcrealP. Qed. -Implicit Arguments le_algP [x y]. +Arguments le_algP [x y]. Prenex Implicits lt_algP le_algP. Lemma ler_to_alg : {mono to_alg : x y / x <= y}. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 2b0ab00..f3ff7c3 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -196,7 +196,7 @@ Arguments Scope Ohm [nat_scope _ group_scope]. Arguments Scope Ohm_group [nat_scope _ group_scope]. Arguments Scope Mho [nat_scope _ group_scope]. Arguments Scope Mho_group [nat_scope _ group_scope]. -Implicit Arguments OhmPredP [n gT x]. +Arguments OhmPredP [n gT x]. Notation "''Ohm_' n ( G )" := (Ohm n G) (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope. @@ -233,7 +233,7 @@ apply: (iffP (dvdn_biglcmP _ _ _)) => eAn x Ax. by apply/eqP; rewrite -order_dvdn eAn. by rewrite order_dvdn eAn. Qed. -Implicit Arguments exponentP [A n]. +Arguments exponentP [A n]. Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1). Proof. @@ -495,7 +495,7 @@ Qed. Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)). Proof. by rewrite inE; apply: andP. Qed. -Implicit Arguments pElemP [p A E]. +Arguments pElemP [p A E]. Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B). Proof. @@ -511,7 +511,7 @@ Proof. by rewrite !inE conjSg abelemJ. Qed. Lemma pnElemP p n A E : reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)). Proof. by rewrite !inE -andbA; apply: (iffP and3P) => [] [-> -> /eqP]. Qed. -Implicit Arguments pnElemP [p n A E]. +Arguments pnElemP [p n A E]. Lemma pnElemPcard p n A E : E \in 'E_p^n(A) -> [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N. @@ -636,7 +636,7 @@ have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS. case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //. by rewrite (eqP oE) dvdn_exp. Qed. -Implicit Arguments nElemP [n G E]. +Arguments nElemP [n G E]. Lemma nElem0 G : 'E^0(G) = [set 1%G]. Proof. @@ -899,18 +899,18 @@ Qed. End ExponentAbelem. -Implicit Arguments LdivP [gT A n x]. -Implicit Arguments exponentP [gT A n]. -Implicit Arguments abelemP [gT p G]. -Implicit Arguments is_abelemP [gT G]. -Implicit Arguments pElemP [gT p A E]. -Implicit Arguments pnElemP [gT p n A E]. -Implicit Arguments nElemP [gT n G E]. -Implicit Arguments nElem1P [gT G E]. -Implicit Arguments pmaxElemP [gT p A E]. -Implicit Arguments pmaxElem_LdivP [gT p G E]. -Implicit Arguments p_rank_geP [gT p n G]. -Implicit Arguments rank_geP [gT n G]. +Arguments LdivP [gT A n x]. +Arguments exponentP [gT A n]. +Arguments abelemP [gT p G]. +Arguments is_abelemP [gT G]. +Arguments pElemP [gT p A E]. +Arguments pnElemP [gT p n A E]. +Arguments nElemP [gT n G E]. +Arguments nElem1P [gT G E]. +Arguments pmaxElemP [gT p A E]. +Arguments pmaxElem_LdivP [gT p G E]. +Arguments p_rank_geP [gT p n G]. +Arguments rank_geP [gT n G]. Section MorphAbelem. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index d9010d5..1c804cc 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -26,7 +26,7 @@ rewrite big_uniq // -(card_uniqP Us) (eq_card sG) -Frobenius_Cauchy. by apply/actsP=> ? _ ?; rewrite !inE. Qed. -Implicit Arguments burnside_formula [gT]. +Arguments burnside_formula [gT]. Section colouring. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 54726be..c461a9e 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -187,7 +187,7 @@ End Injm. End Center. -Implicit Arguments center_idP [gT A]. +Arguments center_idP [gT A]. Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) : G \isog H -> 'Z(G) \isog 'Z(H). diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 1f9bad0..6a390ce 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed. End Commutator_properties. -Implicit Arguments derG1P [gT G]. +Arguments derG1P [gT G]. Lemma der_cont n : GFunctor.continuous (derived_at n). Proof. by move=> aT rT G f; rewrite morphim_der. Qed. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 9a1e451..7663163 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -292,7 +292,7 @@ End Cyclic. Arguments Scope cyclic [_ group_scope]. Arguments Scope generator [_ group_scope group_scope]. Arguments Scope expg_invn [_ group_scope nat_scope]. -Implicit Arguments cyclicP [gT A]. +Arguments cyclicP [gT A]. Prenex Implicits cyclic Zpm generator expg_invn. (* Euler's theorem *) @@ -558,7 +558,7 @@ End Metacyclic. Arguments Scope metacyclic [_ group_scope]. Prenex Implicits metacyclic. -Implicit Arguments metacyclicP [gT A]. +Arguments metacyclicP [gT A]. (* Automorphisms of cyclic groups. *) Section CyclicAutomorphism. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index da65950..3416587 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -246,7 +246,7 @@ have Gg: g \in G by rewrite groupMl ?groupV. rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP). by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->. Qed. -Implicit Arguments normedTI_P [A G L]. +Arguments normedTI_P [A G L]. Lemma normedTI_memJ_P A G L : reflect [/\ A != set0, L \subset G @@ -622,9 +622,9 @@ Qed. End FrobeniusBasics. -Implicit Arguments normedTI_P [gT A G L]. -Implicit Arguments normedTI_memJ_P [gT A G L]. -Implicit Arguments Frobenius_kerP [gT G K]. +Arguments normedTI_P [gT A G L]. +Arguments normedTI_memJ_P [gT A G L]. +Arguments Frobenius_kerP [gT G K]. Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) : K ><| H = G -> N <| G -> coprime #|K| #|H| /\ H :!=: 1%g -> diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 6dcd833..1dc6a35 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -212,7 +212,7 @@ Qed. End Subnormal. -Implicit Arguments subnormalP [gT G H]. +Arguments subnormalP [gT H G]. Prenex Implicits subnormalP. Section MorphSubNormal. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index e5c2d4f..06cf329 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1649,4 +1649,4 @@ Qed. End SCN. -Implicit Arguments SCN_P [gT G A].
\ No newline at end of file +Arguments SCN_P [gT G A].
\ No newline at end of file diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index b595530..d383aa7 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -170,7 +170,7 @@ Proof. exact: partn_eq1 (cardG_gt0 G). Qed. Lemma pgroupP pi G : reflect (forall p, prime p -> p %| #|G| -> p \in pi) (pi.-group G). Proof. exact: pnatP. Qed. -Implicit Arguments pgroupP [pi G]. +Arguments pgroupP [pi G]. Lemma pgroup1 pi : pi.-group [1 gT]. Proof. by rewrite /pgroup cards1. Qed. @@ -679,8 +679,8 @@ Qed. End PgroupProps. -Implicit Arguments pgroupP [gT pi G]. -Implicit Arguments constt1P [gT pi x]. +Arguments pgroupP [gT pi G]. +Arguments constt1P [gT pi x]. Prenex Implicits pgroupP constt1P. Section NormalHall. @@ -1302,8 +1302,8 @@ Qed. End EqPcore. -Implicit Arguments sdprod_Hall_pcoreP [gT pi G H]. -Implicit Arguments sdprod_Hall_p'coreP [gT pi G H]. +Arguments sdprod_Hall_pcoreP [pi gT H G]. +Arguments sdprod_Hall_p'coreP [gT pi H G]. Section Injm. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index ae60ce0..c0ab34b 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -187,7 +187,7 @@ End NTransitive. Arguments Scope dtuple_on [_ nat_scope group_scope]. Arguments Scope ntransitive [_ _ nat_scope group_scope group_scope action_scope]. -Implicit Arguments n_act [gT sT n]. +Arguments n_act [gT sT] _ [n]. Notation "n .-dtuple ( S )" := (dtuple_on n S) (at level 8, format "n .-dtuple ( S )") : set_scope. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 941b488..64e8927 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -678,7 +678,7 @@ Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F : -> K' (\big[op/idx]_(i <- r | P i) F i). Proof. by case. Qed. -Implicit Arguments big_load [R K' I]. +Arguments big_load [R] K [K'] idx op [I]. Section Elim3. @@ -708,8 +708,8 @@ Proof. by apply: big_rec3 => i x1 x2 x3 /K_F; apply: Kop. Qed. End Elim3. -Implicit Arguments big_rec3 [R1 R2 R3 id1 op1 id2 op2 id3 op3 I r P F1 F2 F3]. -Implicit Arguments big_ind3 [R1 R2 R3 id1 op1 id2 op2 id3 op3 I r P F1 F2 F3]. +Arguments big_rec3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ [I r P F1 F2 F3]. +Arguments big_ind3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ _ [I r P F1 F2 F3]. Section Elim2. @@ -738,9 +738,9 @@ Proof. by rewrite unlock; elim: r => //= i r <-; rewrite -f_op -fun_if. Qed. End Elim2. -Implicit Arguments big_rec2 [R1 R2 id1 op1 id2 op2 I r P F1 F2]. -Implicit Arguments big_ind2 [R1 R2 id1 op1 id2 op2 I r P F1 F2]. -Implicit Arguments big_morph [R1 R2 id1 op1 id2 op2 I]. +Arguments big_rec2 [R1 R2] K [id1 op1 id2 op2] _ [I r P F1 F2]. +Arguments big_ind2 [R1 R2] K [id1 op1 id2 op2] _ _ [I r P F1 F2]. +Arguments big_morph [R1 R2] f [id1 op1 id2 op2] _ _ [I]. Section Elim1. @@ -773,10 +773,10 @@ Proof. exact: big_morph. Qed. End Elim1. -Implicit Arguments big_rec [R idx op I r P F]. -Implicit Arguments big_ind [R idx op I r P F]. -Implicit Arguments eq_big_op [R idx op I]. -Implicit Arguments big_endo [R idx op I]. +Arguments big_rec [R] K [idx op] _ [I r P F]. +Arguments big_ind [R] K [idx op] _ _ [I r P F]. +Arguments eq_big_op [R] K [idx op] op' _ _ _ [I]. +Arguments big_endo [R] f [idx op] _ _ [I]. Section Extensionality. @@ -1306,7 +1306,7 @@ Proof. rewrite !(big_mkcond _ _ _ F) -big_split. by apply: eq_bigr => i; case: (a i); rewrite !simpm. Qed. -Implicit Arguments bigID [I r]. +Arguments bigID [I r]. Lemma bigU (I : finType) (A B : pred I) F : [disjoint A & B] -> @@ -1325,7 +1325,7 @@ Proof. move=> Pj; rewrite (bigID (pred1 j)); congr (_ * _). by apply: big_pred1 => i; rewrite /= andbC; case: eqP => // ->. Qed. -Implicit Arguments bigD1 [I P F]. +Arguments bigD1 [I] j [P F]. Lemma bigD1_seq (I : eqType) (r : seq I) j F : j \in r -> uniq r -> @@ -1338,7 +1338,7 @@ Proof. move=> Aj; rewrite (cardD1 j) [j \in A]Aj; congr (_ + _). by apply: eq_card => i; rewrite inE /= andbC. Qed. -Implicit Arguments cardD1x [I A]. +Arguments cardD1x [I A]. Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F : (forall i, P i -> Q (p i)) -> @@ -1356,7 +1356,7 @@ rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i. by rewrite andbA. Qed. -Implicit Arguments partition_big [I J P F]. +Arguments partition_big [I J P] p Q [F]. Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : (forall i, P i -> h (h' i) = i) -> @@ -1372,7 +1372,7 @@ rewrite {}IH => [|j]; [apply: eq_bigl => j | by case/andP; auto]. rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _). by apply/eqP/eqP=> [<-|->] //; rewrite h'K. Qed. -Implicit Arguments reindex_onto [I J P F]. +Arguments reindex_onto [I J] h h' [P F]. Lemma reindex (I J : finType) (h : J -> I) (P : pred I) F : {on [pred i | P i], bijective h} -> @@ -1381,12 +1381,12 @@ Proof. case=> h' hK h'K; rewrite (reindex_onto h h' h'K). by apply: eq_bigl => j; rewrite !inE; case Pi: (P _); rewrite //= hK ?eqxx. Qed. -Implicit Arguments reindex [I J P F]. +Arguments reindex [I J] h [P F]. Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F : injective h -> \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j)) F (h j). Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed. -Implicit Arguments reindex_inj [I h P F]. +Arguments reindex_inj [I h P F]. Lemma big_nat_rev m n P F : \big[*%M/1]_(m <= i < n | P i) F i @@ -1430,7 +1430,7 @@ rewrite !pair_big_dep (reindex_onto (p _ _) (p _ _)) => [|[]] //=. apply: eq_big => [] [j i] //=; symmetry; rewrite eqxx andbT andb_idl //. by case/andP; apply: PQxQ. Qed. -Implicit Arguments exchange_big_dep [I J rI rJ P Q F]. +Arguments exchange_big_dep [I J rI rJ P Q] xQ [F]. Lemma exchange_big I J rI rJ (P : pred I) (Q : pred J) F : \big[*%M/1]_(i <- rI | P i) \big[*%M/1]_(j <- rJ | Q j) F i j = @@ -1453,7 +1453,7 @@ rewrite big_seq_cond /= (exchange_big_dep xQ) => [|i j]; last first. rewrite 2!(big_seq_cond _ _ _ xQ); apply: eq_bigr => j /andP[-> _] /=. by rewrite [rhs in _ = rhs]big_seq_cond; apply: eq_bigl => i; rewrite -andbA. Qed. -Implicit Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q F]. +Arguments exchange_big_dep_nat [m1 n1 m2 n2 P Q] xQ [F]. Lemma exchange_big_nat m1 n1 m2 n2 (P Q : pred nat) F : \big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q j) F i j = @@ -1467,58 +1467,58 @@ End Abelian. End MonoidProperties. -Implicit Arguments big_filter [R op idx I]. -Implicit Arguments big_filter_cond [R op idx I]. -Implicit Arguments congr_big [R op idx I r1 P1 F1]. -Implicit Arguments eq_big [R op idx I r P1 F1]. -Implicit Arguments eq_bigl [R op idx I r P1]. -Implicit Arguments eq_bigr [R op idx I r P F1]. -Implicit Arguments eq_big_idx [R op idx idx' I P F]. -Implicit Arguments big_seq_cond [R op idx I r]. -Implicit Arguments eq_big_seq [R op idx I r F1]. -Implicit Arguments congr_big_nat [R op idx m1 n1 P1 F1]. -Implicit Arguments big_map [R op idx I J r]. -Implicit Arguments big_nth [R op idx I r]. -Implicit Arguments big_catl [R op idx I r1 r2 P F]. -Implicit Arguments big_catr [R op idx I r1 r2 P F]. -Implicit Arguments big_geq [R op idx m n P F]. -Implicit Arguments big_ltn_cond [R op idx m n P F]. -Implicit Arguments big_ltn [R op idx m n F]. -Implicit Arguments big_addn [R op idx]. -Implicit Arguments big_mkord [R op idx n]. -Implicit Arguments big_nat_widen [R op idx] . -Implicit Arguments big_ord_widen_cond [R op idx n1]. -Implicit Arguments big_ord_widen [R op idx n1]. -Implicit Arguments big_ord_widen_leq [R op idx n1]. -Implicit Arguments big_ord_narrow_cond [R op idx n1 n2 P F]. -Implicit Arguments big_ord_narrow_cond_leq [R op idx n1 n2 P F]. -Implicit Arguments big_ord_narrow [R op idx n1 n2 F]. -Implicit Arguments big_ord_narrow_leq [R op idx n1 n2 F]. -Implicit Arguments big_mkcond [R op idx I r]. -Implicit Arguments big1_eq [R op idx I]. -Implicit Arguments big1_seq [R op idx I]. -Implicit Arguments big1 [R op idx I]. -Implicit Arguments big_pred1 [R op idx I P F]. -Implicit Arguments eq_big_perm [R op idx I r1 P F]. -Implicit Arguments big_uniq [R op idx I F]. -Implicit Arguments big_rem [R op idx I r P F]. -Implicit Arguments bigID [R op idx I r]. -Implicit Arguments bigU [R op idx I]. -Implicit Arguments bigD1 [R op idx I P F]. -Implicit Arguments bigD1_seq [R op idx I r F]. -Implicit Arguments partition_big [R op idx I J P F]. -Implicit Arguments reindex_onto [R op idx I J P F]. -Implicit Arguments reindex [R op idx I J P F]. -Implicit Arguments reindex_inj [R op idx I h P F]. -Implicit Arguments pair_big_dep [R op idx I J]. -Implicit Arguments pair_big [R op idx I J]. -Implicit Arguments big_allpairs [R op idx I1 I2 r1 r2 F]. -Implicit Arguments exchange_big_dep [R op idx I J rI rJ P Q F]. -Implicit Arguments exchange_big_dep_nat [R op idx m1 n1 m2 n2 P Q F]. -Implicit Arguments big_ord_recl [R op idx]. -Implicit Arguments big_ord_recr [R op idx]. -Implicit Arguments big_nat_recl [R op idx]. -Implicit Arguments big_nat_recr [R op idx]. +Arguments big_filter [R idx op I]. +Arguments big_filter_cond [R idx op I]. +Arguments congr_big [R idx op I r1] r2 [P1] P2 [F1] F2. +Arguments eq_big [R idx op I r P1] P2 [F1] F2. +Arguments eq_bigl [R idx op I r P1] P2. +Arguments eq_bigr [R idx op I r P F1] F2. +Arguments eq_big_idx [R idx op idx' I] i0 [P F]. +Arguments big_seq_cond [R idx op I r]. +Arguments eq_big_seq [R idx op I r F1] F2. +Arguments congr_big_nat [R idx op m1 n1] m2 n2 [P1] P2 [F1] F2. +Arguments big_map [R idx op I J] h [r]. +Arguments big_nth [R idx op I] x0 [r]. +Arguments big_catl [R idx op I r1 r2 P F]. +Arguments big_catr [R idx op I r1 r2 P F]. +Arguments big_geq [R idx op m n P F]. +Arguments big_ltn_cond [R idx op m n P F]. +Arguments big_ltn [R idx op m n F]. +Arguments big_addn [R idx op]. +Arguments big_mkord [R idx op n]. +Arguments big_nat_widen [R idx op] . +Arguments big_ord_widen_cond [R idx op n1]. +Arguments big_ord_widen [R idx op n1]. +Arguments big_ord_widen_leq [R idx op n1]. +Arguments big_ord_narrow_cond [R idx op n1 n2 P F]. +Arguments big_ord_narrow_cond_leq [R idx op n1 n2 P F]. +Arguments big_ord_narrow [R idx op n1 n2 F]. +Arguments big_ord_narrow_leq [R idx op n1 n2 F]. +Arguments big_mkcond [R idx op I r]. +Arguments big1_eq [R idx op I]. +Arguments big1_seq [R idx op I]. +Arguments big1 [R idx op I]. +Arguments big_pred1 [R idx op I] i [P F]. +Arguments eq_big_perm [R idx op I r1] r2 [P F]. +Arguments big_uniq [R idx op I] r [F]. +Arguments big_rem [R idx op I r] x [P F]. +Arguments bigID [R idx op I r]. +Arguments bigU [R idx op I]. +Arguments bigD1 [R idx op I] j [P F]. +Arguments bigD1_seq [R idx op I r] j [F]. +Arguments partition_big [R idx op I J P] p Q [F]. +Arguments reindex_onto [R idx op I J] h h' [P F]. +Arguments reindex [R idx op I J] h [P F]. +Arguments reindex_inj [R idx op I h P F]. +Arguments pair_big_dep [R idx op I J]. +Arguments pair_big [R idx op I J]. +Arguments big_allpairs [R idx op I1 I2 r1 r2 F]. +Arguments exchange_big_dep [R idx op I J rI rJ P Q] xQ [F]. +Arguments exchange_big_dep_nat [R idx op m1 n1 m2 n2 P Q] xQ [F]. +Arguments big_ord_recl [R idx op]. +Arguments big_ord_recr [R idx op]. +Arguments big_nat_recl [R idx op]. +Arguments big_nat_recr [R idx op]. Section Distributivity. @@ -1614,13 +1614,13 @@ Proof. by rewrite bigA_distr_big; apply: eq_bigl => ?; apply/familyP. Qed. End Distributivity. -Implicit Arguments big_distrl [R zero times plus I r]. -Implicit Arguments big_distrr [R zero times plus I r]. -Implicit Arguments big_distr_big_dep [R zero one times plus I J]. -Implicit Arguments big_distr_big [R zero one times plus I J]. -Implicit Arguments bigA_distr_big_dep [R zero one times plus I J]. -Implicit Arguments bigA_distr_big [R zero one times plus I J]. -Implicit Arguments bigA_distr_bigA [R zero one times plus I J]. +Arguments big_distrl [R zero times plus I r]. +Arguments big_distrr [R zero times plus I r]. +Arguments big_distr_big_dep [R zero one times plus I J]. +Arguments big_distr_big [R zero one times plus I J]. +Arguments bigA_distr_big_dep [R zero one times plus I J]. +Arguments bigA_distr_big [R zero one times plus I J]. +Arguments bigA_distr_bigA [R zero one times plus I J]. Section BigBool. @@ -1715,11 +1715,11 @@ Proof. by move=> Fpos; apply: prodn_cond_gt0. Qed. Lemma leq_bigmax_cond (I : finType) (P : pred I) F i0 : P i0 -> F i0 <= \max_(i | P i) F i. Proof. by move=> Pi0; rewrite (bigD1 i0) ?leq_maxl. Qed. -Implicit Arguments leq_bigmax_cond [I P F]. +Arguments leq_bigmax_cond [I P F]. Lemma leq_bigmax (I : finType) F (i0 : I) : F i0 <= \max_i F i. Proof. exact: leq_bigmax_cond. Qed. -Implicit Arguments leq_bigmax [I F]. +Arguments leq_bigmax [I F]. Lemma bigmax_leqP (I : finType) (P : pred I) m F : reflect (forall i, P i -> F i <= m) (\max_(i | P i) F i <= m). @@ -1732,7 +1732,7 @@ Qed. Lemma bigmax_sup (I : finType) i0 (P : pred I) m F : P i0 -> m <= F i0 -> m <= \max_(i | P i) F i. Proof. by move=> Pi0 le_m_Fi0; apply: leq_trans (leq_bigmax_cond i0 Pi0). Qed. -Implicit Arguments bigmax_sup [I P m F]. +Arguments bigmax_sup [I] i0 [P m F]. Lemma bigmax_eq_arg (I : finType) i0 (P : pred I) F : P i0 -> \max_(i | P i) F i = F [arg max_(i > i0 | P i) F i]. @@ -1740,7 +1740,7 @@ Proof. move=> Pi0; case: arg_maxP => //= i Pi maxFi. by apply/eqP; rewrite eqn_leq leq_bigmax_cond // andbT; apply/bigmax_leqP. Qed. -Implicit Arguments bigmax_eq_arg [I P F]. +Arguments bigmax_eq_arg [I] i0 [P F]. Lemma eq_bigmax_cond (I : finType) (A : pred I) F : #|A| > 0 -> {i0 | i0 \in A & \max_(i in A) F i = F i0}. @@ -1769,7 +1769,7 @@ Lemma biglcmn_sup (I : finType) i0 (P : pred I) F m : Proof. by move=> Pi0 m_Fi0; rewrite (dvdn_trans m_Fi0) // (bigD1 i0) ?dvdn_lcml. Qed. -Implicit Arguments biglcmn_sup [I P F m]. +Arguments biglcmn_sup [I] i0 [P F m]. Lemma dvdn_biggcdP (I : finType) (P : pred I) F m : reflect (forall i, P i -> m %| F i) (m %| \big[gcdn/0]_(i | P i) F i). @@ -1782,6 +1782,6 @@ Qed. Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m : P i0 -> F i0 %| m -> \big[gcdn/0]_(i | P i) F i %| m. Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed. -Implicit Arguments biggcdn_inf [I P F m]. +Arguments biggcdn_inf [I] i0 [P F m]. Unset Implicit Arguments. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index a696bbd..b5c2391 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -193,7 +193,7 @@ Qed. End Def. End GenTree. -Implicit Arguments GenTree.codeK []. +Arguments GenTree.codeK : clear implicits. Definition tree_eqMixin (T : eqType) := PcanEqMixin (GenTree.codeK T). Canonical tree_eqType (T : eqType) := EqType (GenTree.tree T) (tree_eqMixin T). @@ -558,7 +558,7 @@ Export Countable.Exports. Definition unpickle T := Countable.unpickle (Countable.class T). Definition pickle T := Countable.pickle (Countable.class T). -Implicit Arguments unpickle [T]. +Arguments unpickle [T]. Prenex Implicits pickle unpickle. Section CountableTheory. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 4172430..59c19ce 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -130,11 +130,11 @@ rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0. by rewrite addnC divn_small // ltn_pmul2l. Qed. -Implicit Arguments divnMl [p m d]. +Arguments divnMl [p m d]. Lemma divnMr p m d : p > 0 -> m * p %/ (d * p) = m %/ d. Proof. by move=> p_gt0; rewrite -!(mulnC p) divnMl. Qed. -Implicit Arguments divnMr [p m d]. +Arguments divnMr [p m d]. Lemma ltn_mod m d : (m %% d < d) = (0 < d). Proof. by case: d => // d; rewrite modn_def; case: edivnP. Qed. @@ -302,7 +302,7 @@ Proof. apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl. by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0. Qed. -Implicit Arguments dvdnP [d m]. +Arguments dvdnP [d m]. Prenex Implicits dvdnP. Lemma dvdn0 d : d %| 0. @@ -401,11 +401,11 @@ Qed. Lemma dvdn_pmul2l p d m : 0 < p -> (p * d %| p * m) = (d %| m). Proof. by case: p => // p _; rewrite /dvdn -muln_modr // muln_eq0. Qed. -Implicit Arguments dvdn_pmul2l [p m d]. +Arguments dvdn_pmul2l [p d m]. Lemma dvdn_pmul2r p d m : 0 < p -> (d * p %| m * p) = (d %| m). Proof. by move=> p_gt0; rewrite -!(mulnC p) dvdn_pmul2l. Qed. -Implicit Arguments dvdn_pmul2r [p m d]. +Arguments dvdn_pmul2r [p d m]. Lemma dvdn_divLR p d m : 0 < p -> p %| d -> (d %/ p %| m) = (d %| m * p). Proof. by move=> /(@dvdn_pmul2r p _ m) <- /divnK->. Qed. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 3e8230e..9772b84 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -147,7 +147,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Implicit Arguments eqP [T x y]. +Arguments eqP [T x y]. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -230,8 +230,8 @@ Proof. by rewrite eq_sym; apply: ifN. Qed. End Contrapositives. -Implicit Arguments memPn [T1 A x]. -Implicit Arguments memPnC [T1 A x]. +Arguments memPn [T1 A x]. +Arguments memPnC [T1 A x]. Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2. Proof. @@ -339,9 +339,9 @@ Proof. by case: eqP; [left | right]. Qed. End EqPred. -Implicit Arguments predU1P [T x y b]. -Implicit Arguments pred2P [T T2 x y z u]. -Implicit Arguments predD1P [T x y b]. +Arguments predU1P [T x y b]. +Arguments pred2P [T T2 x y z u]. +Arguments predD1P [T x y b]. Prenex Implicits pred1 pred2 pred3 pred4 predU1 predC1 predD1 predU1P. Notation "[ 'predU1' x & A ]" := (predU1 x [mem A]) @@ -491,7 +491,7 @@ Structure subType : Type := SubType { _ : forall x Px, val (@Sub x Px) = x }. -Implicit Arguments Sub [s]. +Arguments Sub [s]. Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed. Definition vrefl_rect := vrefl. @@ -572,14 +572,14 @@ Qed. End SubType. -Implicit Arguments SubType [T P]. -Implicit Arguments Sub [T P s]. -Implicit Arguments vrefl [T P]. -Implicit Arguments vrefl_rect [T P]. -Implicit Arguments clone_subType [T P sT c Urec cK]. -Implicit Arguments insub [T P sT]. -Implicit Arguments insubT [T sT x]. -Implicit Arguments val_inj [T P sT]. +Arguments SubType [T P]. +Arguments Sub [T P s]. +Arguments vrefl [T P]. +Arguments vrefl_rect [T P]. +Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. +Arguments insub [T P sT]. +Arguments insubT [T] P [sT x]. +Arguments val_inj [T P sT]. Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj. Local Notation inlined_sub_rect := @@ -610,7 +610,7 @@ Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id) Definition NewType T U v c Urec := let Urec' P IH := Urec P (fun x : T => IH x isT : P _) in SubType U v (fun x _ => c x) Urec'. -Implicit Arguments NewType [T U]. +Arguments NewType [T U]. Notation "[ 'newType' 'for' v ]" := (NewType v _ inlined_new_rect vrefl_rect) (at level 0, only parsing) : form_scope. @@ -622,7 +622,7 @@ Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl) (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope. Definition innew T nT x := @Sub T predT nT x (erefl true). -Implicit Arguments innew [T nT]. +Arguments innew [T nT]. Prenex Implicits innew. Lemma innew_val T nT : cancel val (@innew T nT). @@ -713,7 +713,7 @@ Proof. by []. Qed. End SubEqType. -Implicit Arguments val_eqP [T P sT x y]. +Arguments val_eqP [T P sT x y]. Prenex Implicits val_eqP. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) @@ -757,7 +757,7 @@ Proof. by case/andP. Qed. End ProdEqType. -Implicit Arguments pair_eqP [T1 T2]. +Arguments pair_eqP [T1 T2]. Prenex Implicits pair_eqP. @@ -787,7 +787,7 @@ End OptionEqType. Definition tag := projS1. Definition tagged I T_ : forall u, T_(tag u) := @projS2 I [eta T_]. Definition Tagged I i T_ x := @existS I [eta T_] i x. -Implicit Arguments Tagged [I i]. +Arguments Tagged [I i]. Prenex Implicits tag tagged Tagged. Section TaggedAs. @@ -834,7 +834,7 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed. End TagEqType. -Implicit Arguments tag_eqP [I T_ x y]. +Arguments tag_eqP [I T_ x y]. Prenex Implicits tag_eqP. Section SumEqType. @@ -858,5 +858,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed. End SumEqType. -Implicit Arguments sum_eqP [T1 T2 x y]. +Arguments sum_eqP [T1 T2 x y]. Prenex Implicits sum_eqP. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 43ba42a..8b85320 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -147,8 +147,8 @@ End PlainTheory. Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). -Implicit Arguments familyP [aT rT pT F f]. -Implicit Arguments ffun_onP [aT rT R f]. +Arguments familyP [aT rT pT F f]. +Arguments ffun_onP [aT rT R f]. (*****************************************************************************) @@ -213,7 +213,7 @@ Qed. End EqTheory. -Implicit Arguments supportP [aT rT y D g]. +Arguments supportP [aT rT y D g]. Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))). Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)). diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index dfba3c7..baf5efe 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -224,9 +224,9 @@ Notation closure e a := (closure_mem e (mem a)). Prenex Implicits connect root roots. -Implicit Arguments dfsP [T g x y]. -Implicit Arguments connectP [T e x y]. -Implicit Arguments rootP [T e x y]. +Arguments dfsP [T g x y]. +Arguments connectP [T e x y]. +Arguments rootP [T e] _ [x y]. Notation fconnect f := (connect (coerced_frel f)). Notation froot f := (root (coerced_frel f)). @@ -770,7 +770,7 @@ Notation "@ 'fun_adjunction' T T' h f f' a" := (@rel_adjunction T T' h (frel f) (frel f') a) (at level 10, T, T', h, f, f', a at level 8, only parsing) : type_scope. -Implicit Arguments intro_adjunction [T T' h e e' a]. -Implicit Arguments adjunction_n_comp [T T' e e' a]. +Arguments intro_adjunction [T T' h e e'] _ [a]. +Arguments adjunction_n_comp [T T'] h [e e'] _ _ [a]. Unset Implicit Arguments. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index dc964b5..3f99e9f 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -243,7 +243,7 @@ End BasicSetTheory. Definition inE := (in_set, inE). -Implicit Arguments set0 [T]. +Arguments set0 [T]. Prenex Implicits set0. Hint Resolve in_setT. @@ -827,7 +827,7 @@ Proof. apply: (iffP subsetP) => [sAB | <- x /setIP[] //]. by apply/setP=> x; rewrite inE; apply/andb_idr/sAB. Qed. -Implicit Arguments setIidPl [A B]. +Arguments setIidPl [A B]. Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A). Proof. by rewrite setIC; apply: setIidPl. Qed. @@ -955,26 +955,26 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. End setOps. -Implicit Arguments set1P [T x a]. -Implicit Arguments set1_inj [T]. -Implicit Arguments set2P [T x a b]. -Implicit Arguments setIdP [T x pA pB]. -Implicit Arguments setIP [T x A B]. -Implicit Arguments setU1P [T x a B]. -Implicit Arguments setD1P [T x A b]. -Implicit Arguments setUP [T x A B]. -Implicit Arguments setDP [T x A B]. -Implicit Arguments cards1P [T A]. -Implicit Arguments setCP [T x A]. -Implicit Arguments setIidPl [T A B]. -Implicit Arguments setIidPr [T A B]. -Implicit Arguments setUidPl [T A B]. -Implicit Arguments setUidPr [T A B]. -Implicit Arguments setDidPl [T A B]. -Implicit Arguments subsetIP [T A B C]. -Implicit Arguments subUsetP [T A B C]. -Implicit Arguments subsetDP [T A B C]. -Implicit Arguments subsetD1P [T A B x]. +Arguments set1P [T x a]. +Arguments set1_inj [T]. +Arguments set2P [T x a b]. +Arguments setIdP [T x pA pB]. +Arguments setIP [T x A B]. +Arguments setU1P [T x a B]. +Arguments setD1P [T x A b]. +Arguments setUP [T x A B]. +Arguments setDP [T A B x]. +Arguments cards1P [T A]. +Arguments setCP [T x A]. +Arguments setIidPl [T A B]. +Arguments setIidPr [T A B]. +Arguments setUidPl [T A B]. +Arguments setUidPr [T A B]. +Arguments setDidPl [T A B]. +Arguments subsetIP [T A B C]. +Arguments subUsetP [T A B C]. +Arguments subsetDP [T A B C]. +Arguments subsetD1P [T A B x]. Prenex Implicits set1 set1_inj. Prenex Implicits set1P set2P setU1P setD1P setIdP setIP setUP setDP. Prenex Implicits cards1P setCP setIidPl setIidPr setUidPl setUidPr setDidPl. @@ -1018,7 +1018,7 @@ Proof. by rewrite cardsE cardX. Qed. End CartesianProd. -Implicit Arguments setXP [x1 x2 fT1 fT2 A1 A2]. +Arguments setXP [fT1 fT2 A1 A2 x1 x2]. Prenex Implicits setXP. Local Notation imset_def := @@ -1365,8 +1365,8 @@ Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed. End FunImage. -Implicit Arguments imsetP [aT rT f D y]. -Implicit Arguments imset2P [aT aT2 rT f2 D1 D2 y]. +Arguments imsetP [aT rT f D y]. +Arguments imset2P [aT aT2 rT f2 D1 D2 y]. Prenex Implicits imsetP imset2P. Section BigOps. @@ -1439,11 +1439,11 @@ Proof. by apply: partition_big => i Ai; apply/imsetP; exists i. Qed. End BigOps. -Implicit Arguments big_setID [R idx aop I A]. -Implicit Arguments big_setD1 [R idx aop I A F]. -Implicit Arguments big_setU1 [R idx aop I A F]. -Implicit Arguments big_imset [R idx aop h I J A]. -Implicit Arguments partition_big_imset [R idx aop I J]. +Arguments big_setID [R idx aop I A]. +Arguments big_setD1 [R idx aop I] a [A F]. +Arguments big_setU1 [R idx aop I] a [A F]. +Arguments big_imset [R idx aop I J h A]. +Arguments partition_big_imset [R idx aop I J]. Section Fun2Set1. @@ -1499,7 +1499,7 @@ Proof. by move=> fK gK; apply: can2_in_imset_pre; apply: in1W. Qed. End CardFunImage. -Implicit Arguments imset_injP [aT rT f D]. +Arguments imset_injP [aT rT f D]. Lemma on_card_preimset (aT rT : finType) (f : aT -> rT) (R : pred rT) : {on R, bijective f} -> #|f @^-1: R| = #|R|. @@ -1701,14 +1701,14 @@ Proof. by apply: setC_inj; rewrite !setC_bigcap bigcup_seq. Qed. End BigSetOps. -Implicit Arguments bigcup_sup [T I P F]. -Implicit Arguments bigcup_max [T I U P F]. -Implicit Arguments bigcupP [T I x P F]. -Implicit Arguments bigcupsP [T I U P F]. -Implicit Arguments bigcap_inf [T I P F]. -Implicit Arguments bigcap_min [T I U P F]. -Implicit Arguments bigcapP [T I x P F]. -Implicit Arguments bigcapsP [T I U P F]. +Arguments bigcup_sup [T I] j [P F]. +Arguments bigcup_max [T I] j [U P F]. +Arguments bigcupP [T I x P F]. +Arguments bigcupsP [T I U P F]. +Arguments bigcap_inf [T I] j [P F]. +Arguments bigcap_min [T I] j [U P F]. +Arguments bigcapP [T I x P F]. +Arguments bigcapsP [T I U P F]. Prenex Implicits bigcupP bigcupsP bigcapP bigcapsP. Section ImsetCurry. @@ -2088,11 +2088,11 @@ End Transversals. End Partitions. -Implicit Arguments trivIsetP [T P]. -Implicit Arguments big_trivIset_cond [T R idx op K E]. -Implicit Arguments set_partition_big_cond [T R idx op D K E]. -Implicit Arguments big_trivIset [T R idx op E]. -Implicit Arguments set_partition_big [T R idx op D E]. +Arguments trivIsetP [T P]. +Arguments big_trivIset_cond [T R idx op] P [K E]. +Arguments set_partition_big_cond [T R idx op] P [D K E]. +Arguments big_trivIset [T R idx op] P [E]. +Arguments set_partition_big [T R idx op] P [D E]. Prenex Implicits cover trivIset partition pblock trivIsetP. @@ -2141,7 +2141,7 @@ apply: (iffP forallP) => [minA | [PA minA] B]. by move=> B PB sBA; have:= minA B; rewrite PB sBA /= eqb_id => /eqP. by apply/implyP=> sBA; apply/eqP; apply/eqP/idP=> [-> // | /minA]; apply. Qed. -Implicit Arguments minsetP [P A]. +Arguments minsetP [P A]. Lemma minsetp P A : minset P A -> P A. Proof. by case/minsetP. Qed. @@ -2212,7 +2212,7 @@ Qed. End MaxSetMinSet. -Implicit Arguments minsetP [T P A]. -Implicit Arguments maxsetP [T P A]. +Arguments minsetP [T P A]. +Arguments maxsetP [T P A]. Prenex Implicits minset maxset minsetP maxsetP. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 719a267..1446fbd 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -820,13 +820,13 @@ End OpsTheory. Hint Resolve subxx_hint. -Implicit Arguments pred0P [T P]. -Implicit Arguments pred0Pn [T P]. -Implicit Arguments subsetP [T A B]. -Implicit Arguments subsetPn [T A B]. -Implicit Arguments subset_eqP [T A B]. -Implicit Arguments card_uniqP [T s]. -Implicit Arguments properP [T A B]. +Arguments pred0P [T P]. +Arguments pred0Pn [T P]. +Arguments subsetP [T A B]. +Arguments subsetPn [T A B]. +Arguments subset_eqP [T A B]. +Arguments card_uniqP [T s]. +Arguments properP [T A B]. Prenex Implicits pred0P pred0Pn subsetP subsetPn subset_eqP card_uniqP. (**********************************************************************) @@ -919,14 +919,14 @@ Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed. End Quantifiers. -Implicit Arguments forallP [T P]. -Implicit Arguments eqfunP [T rT f1 f2]. -Implicit Arguments forall_inP [T D P]. -Implicit Arguments eqfun_inP [T rT D f1 f2]. -Implicit Arguments existsP [T P]. -Implicit Arguments exists_eqP [T rT f1 f2]. -Implicit Arguments exists_inP [T D P]. -Implicit Arguments exists_eq_inP [T rT D f1 f2]. +Arguments forallP [T P]. +Arguments eqfunP [T rT f1 f2]. +Arguments forall_inP [T D P]. +Arguments eqfun_inP [T rT D f1 f2]. +Arguments existsP [T P]. +Arguments exists_eqP [T rT f1 f2]. +Arguments exists_inP [T D P]. +Arguments exists_eq_inP [T rT D f1 f2]. Section Extrema. @@ -1184,15 +1184,15 @@ Qed. End Image. Prenex Implicits codom iinv. -Implicit Arguments imageP [T T' f A y]. -Implicit Arguments codomP [T T' f y]. +Arguments imageP [T T' f A y]. +Arguments codomP [T T' f y]. Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) : reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]). Proof. by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *. Qed. -Implicit Arguments flatten_imageP [aT rT A P y]. +Arguments flatten_imageP [aT rT A P y]. Section CardFunImage. @@ -1240,7 +1240,7 @@ Qed. End CardFunImage. -Implicit Arguments image_injP [T T' f A]. +Arguments image_injP [T T' f A]. Section FinCancel. @@ -1748,8 +1748,8 @@ Qed. End EnumRank. -Implicit Arguments enum_val_inj [[T] [A] x1 x2]. -Implicit Arguments enum_rank_inj [[T] x1 x2]. +Arguments enum_val_inj {T A} [x1 x2]. +Arguments enum_rank_inj {T} [x1 x2]. Prenex Implicits enum_val enum_rank. Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i. @@ -1963,10 +1963,10 @@ Lemma lift0 (i : 'I_n') : lift ord0 i = i.+1 :> nat. Proof. by []. Qed. End OrdinalPos. -Implicit Arguments ord0 [[n']]. -Implicit Arguments ord_max [[n']]. -Implicit Arguments inord [[n']]. -Implicit Arguments sub_ord [[n']]. +Arguments ord0 {n'}. +Arguments ord_max {n'}. +Arguments inord {n'}. +Arguments sub_ord {n'}. (* Product of two fintypes which is a fintype *) Section ProdFinType. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 0aafc34..a3e6cac 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -198,7 +198,7 @@ Notation QuotType Q m := (@QuotType_pack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. -Implicit Arguments repr [T qT]. +Arguments repr [T qT]. Prenex Implicits repr. (************************) @@ -248,7 +248,7 @@ Notation piE := (@equal_toE _ _). Canonical equal_to_pi T (qT : quotType T) (x : T) := @EqualTo _ (\pi_qT x) (\pi x) (erefl _). -Implicit Arguments EqualTo [T x equal_val]. +Arguments EqualTo [T x equal_val]. Prenex Implicits EqualTo. Section Morphism. @@ -276,11 +276,11 @@ Lemma pi_morph11 : \pi (h a) = hq (equal_val x). Proof. by rewrite !piE. Qed. End Morphism. -Implicit Arguments pi_morph1 [T qT f fq]. -Implicit Arguments pi_morph2 [T qT g gq]. -Implicit Arguments pi_mono1 [T U qT p pq]. -Implicit Arguments pi_mono2 [T U qT r rq]. -Implicit Arguments pi_morph11 [T U qT qU h hq]. +Arguments pi_morph1 [T qT f fq]. +Arguments pi_morph2 [T qT g gq]. +Arguments pi_mono1 [T U qT p pq]. +Arguments pi_mono2 [T U qT r rq]. +Arguments pi_morph11 [T U qT qU h hq]. Prenex Implicits pi_morph1 pi_morph2 pi_mono1 pi_mono2 pi_morph11. Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 4f3beb4..e649cbe 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -159,7 +159,7 @@ Qed. End Paths. -Implicit Arguments pathP [T e x p]. +Arguments pathP [T e x p]. Prenex Implicits pathP. Section EqPath. @@ -687,9 +687,9 @@ Qed. End EqTrajectory. -Implicit Arguments fpathP [T f x p]. -Implicit Arguments loopingP [T f x n]. -Implicit Arguments trajectP [T f x n y]. +Arguments fpathP [T f x p]. +Arguments loopingP [T f x n]. +Arguments trajectP [T f x n y]. Prenex Implicits traject fpathP loopingP trajectP. Section UniqCycle. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 9494353..648737b 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -349,8 +349,8 @@ case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //]. by rewrite (negPf d_neq1) /= => /eqP. Qed. -Implicit Arguments primeP [p]. -Implicit Arguments primePn [n]. +Arguments primeP [p]. +Arguments primePn [n]. Prenex Implicits primePn primeP. Lemma prime_gt1 p : prime p -> 1 < p. @@ -541,7 +541,7 @@ exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //. by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto. Qed. -Implicit Arguments primePns [n]. +Arguments primePns [n]. Prenex Implicits primePns. Lemma pdivP n : n > 1 -> {p | prime p & p %| n}. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 5574892..a562879 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -780,8 +780,8 @@ End Sequences. Definition rev T (s : seq T) := nosimpl (catrev s [::]). -Implicit Arguments nilP [T s]. -Implicit Arguments all_filterP [T a s]. +Arguments nilP [T s]. +Arguments all_filterP [T a s]. Prenex Implicits size nilP head ohead behead last rcons belast. Prenex Implicits cat take drop rev rot rotr. @@ -875,7 +875,7 @@ Qed. End Rev. -Implicit Arguments revK [[T]]. +Arguments revK {T}. (* Equality and eqType for seq. *) @@ -1287,13 +1287,13 @@ Definition inE := (mem_seq1, in_cons, inE). Prenex Implicits mem_seq1 uniq undup index. -Implicit Arguments eqseqP [T x y]. -Implicit Arguments hasP [T a s]. -Implicit Arguments hasPn [T a s]. -Implicit Arguments allP [T a s]. -Implicit Arguments allPn [T a s]. -Implicit Arguments nseqP [T n x y]. -Implicit Arguments count_memPn [T x s]. +Arguments eqseqP [T x y]. +Arguments hasP [T a s]. +Arguments hasPn [T a s]. +Arguments allP [T a s]. +Arguments allPn [T a s]. +Arguments nseqP [T n x y]. +Arguments count_memPn [T x s]. Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn. Section NthTheory. @@ -1332,9 +1332,9 @@ Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed. Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x). Proof. by case: s. Qed. -Implicit Arguments nthP [T s x]. -Implicit Arguments has_nthP [T a s]. -Implicit Arguments all_nthP [T a s]. +Arguments nthP [T s x]. +Arguments has_nthP [T a s]. +Arguments all_nthP [T a s]. Prenex Implicits nthP has_nthP all_nthP. Definition bitseq := seq bool. @@ -1576,9 +1576,9 @@ End PermSeq. Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2). Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2). -Implicit Arguments perm_eqP [T s1 s2]. -Implicit Arguments perm_eqlP [T s1 s2]. -Implicit Arguments perm_eqrP [T s1 s2]. +Arguments perm_eqP [T s1 s2]. +Arguments perm_eqlP [T s1 s2]. +Arguments perm_eqrP [T s1 s2]. Prenex Implicits perm_eq perm_eqP perm_eqlP perm_eqrP. Hint Resolve perm_eq_refl. @@ -1853,7 +1853,7 @@ Proof. by case/subseqP=> m _ -> Us2; apply: mask_uniq. Qed. End Subseq. Prenex Implicits subseq. -Implicit Arguments subseqP [T s1 s2]. +Arguments subseqP [T s1 s2]. Hint Resolve subseq_refl. @@ -2029,7 +2029,7 @@ Qed. End FilterSubseq. -Implicit Arguments subseq_uniqP [T s1 s2]. +Arguments subseq_uniqP [T s1 s2]. Section EqMap. @@ -2097,7 +2097,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed. End EqMap. -Implicit Arguments mapP [T1 T2 f s y]. +Arguments mapP [T1 T2 f s y]. Prenex Implicits mapP. Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) : @@ -2289,7 +2289,7 @@ Qed. End MakeEqSeq. -Implicit Arguments perm_eq_iotaP [[T] [s] [t]]. +Arguments perm_eq_iotaP {T s t}. Section FoldRight. @@ -2663,7 +2663,7 @@ elim: A => /= [|s A /iffP IH_A]; [by right; case | rewrite mem_cat]. have [s_x|s'x] := @idP (x \in s); first by left; exists s; rewrite ?mem_head. by apply: IH_A => [[t] | [t /predU1P[->|]]]; exists t; rewrite // mem_behead. Qed. -Implicit Arguments flattenP [A x]. +Arguments flattenP [A x]. Lemma flatten_mapP (A : S -> seq T) s y : reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)). @@ -2674,8 +2674,8 @@ Qed. End EqFlatten. -Implicit Arguments flattenP [T A x]. -Implicit Arguments flatten_mapP [S T A s y]. +Arguments flattenP [T A x]. +Arguments flatten_mapP [S T A s y]. Lemma perm_undup_count (T : eqType) (s : seq T) : perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 1c16140..0e5899a 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -174,7 +174,7 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Implicit Arguments eqnP [x y]. +Arguments eqnP [x y]. Prenex Implicits eqnP. Lemma eqnE : eqn = eq_op. Proof. by []. Qed. @@ -394,7 +394,7 @@ apply: (iffP idP); last by elim: n / => // n _ /leq_trans->. elim: n => [|n IHn]; first by case: m. by rewrite leq_eqVlt ltnS => /predU1P[<- // | /IHn]; right. Qed. -Implicit Arguments leP [m n]. +Arguments leP [m n]. Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat. Proof. @@ -411,7 +411,7 @@ Qed. Lemma ltP m n : reflect (m < n)%coq_nat (m < n). Proof. exact leP. Qed. -Implicit Arguments ltP [m n]. +Arguments ltP [m n]. Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat. Proof. exact: (@le_irrelevance m.+1). Qed. @@ -925,19 +925,19 @@ Proof. by rewrite eqn_leq !leq_mul2r -orb_andr -eqn_leq. Qed. Lemma leq_pmul2l m n1 n2 : 0 < m -> (m * n1 <= m * n2) = (n1 <= n2). Proof. by move/prednK=> <-; rewrite leq_mul2l. Qed. -Implicit Arguments leq_pmul2l [m n1 n2]. +Arguments leq_pmul2l [m n1 n2]. Lemma leq_pmul2r m n1 n2 : 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2). Proof. by move/prednK <-; rewrite leq_mul2r. Qed. -Implicit Arguments leq_pmul2r [m n1 n2]. +Arguments leq_pmul2r [m n1 n2]. Lemma eqn_pmul2l m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2). Proof. by move/prednK <-; rewrite eqn_mul2l. Qed. -Implicit Arguments eqn_pmul2l [m n1 n2]. +Arguments eqn_pmul2l [m n1 n2]. Lemma eqn_pmul2r m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2). Proof. by move/prednK <-; rewrite eqn_mul2r. Qed. -Implicit Arguments eqn_pmul2r [m n1 n2]. +Arguments eqn_pmul2r [m n1 n2]. Lemma ltn_mul2l m n1 n2 : (m * n1 < m * n2) = (0 < m) && (n1 < n2). Proof. by rewrite lt0n !ltnNge leq_mul2l negb_or. Qed. @@ -947,11 +947,11 @@ Proof. by rewrite lt0n !ltnNge leq_mul2r negb_or. Qed. Lemma ltn_pmul2l m n1 n2 : 0 < m -> (m * n1 < m * n2) = (n1 < n2). Proof. by move/prednK <-; rewrite ltn_mul2l. Qed. -Implicit Arguments ltn_pmul2l [m n1 n2]. +Arguments ltn_pmul2l [m n1 n2]. Lemma ltn_pmul2r m n1 n2 : 0 < m -> (n1 * m < n2 * m) = (n1 < n2). Proof. by move/prednK <-; rewrite ltn_mul2r. Qed. -Implicit Arguments ltn_pmul2r [m n1 n2]. +Arguments ltn_pmul2r [m n1 n2]. Lemma ltn_Pmull m n : 1 < n -> 0 < m -> m < n * m. Proof. by move=> lt1n m_gt0; rewrite -{1}[m]mul1n ltn_pmul2r. Qed. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 7023bb4..e06bd38 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -266,8 +266,8 @@ Proof. by rewrite -existsb_tnth; apply: existsP. Qed. End TupleQuantifiers. -Implicit Arguments all_tnthP [n T a t]. -Implicit Arguments has_tnthP [n T a t]. +Arguments all_tnthP [n T a t]. +Arguments has_tnthP [n T a t]. Section EqTuple. diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v index 55c7a81..4ba0b47 100644 --- a/mathcomp/ssrtest/elim2.v +++ b/mathcomp/ssrtest/elim2.v @@ -9,7 +9,7 @@ Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F : let s := \big[op/idx]_(i <- r | P i) F i in K s * K' s -> K' s. Proof. by move=> /= [_]. Qed. -Implicit Arguments big_load [R K' idx op I r P F]. +Arguments big_load [R] K [K' idx op I r P F]. Section Elim1. |