diff options
| author | Anton Trunov | 2018-11-27 12:17:47 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-12-04 12:43:20 +0100 |
| commit | 8c82657e7692049dde4a4c44a2ea53d0c4fa7cb5 (patch) | |
| tree | c973a8517cb257f127c60299e86d3f553ba51462 /mathcomp | |
| parent | add6e85884691faef1bf8742e803374815672cc2 (diff) | |
Document parameter names whenever possible
As suggested by @ggonthier
[here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295)
> One of the design ideas for the `Arguments` command was that it would allow
to centralise the documentation of the application of constants.
In that spirit it would be in my opinion better to make as much use of this
as possible, and to document the parameter names whenever possible,
especially that of implicit parameters.
and
[here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163):
> As a general rule, defined functional constants should have maximal prenex
implicit arguments, as this facilitates their use as arguments to functionals,
because this mimics the way function constants are treated in functional
programming languages with Hindley-Milner type inference. Conversely, lemmas and
theorems should have on-demand implicit arguments, possibly interspersed with
explicit ones, as it's fairly common for other lemmas to have universally
quantified premises; also, this makes it easier to specify such arguments with
the apply: tactic. This policy may be amended for lemmas that are used as
functional arguments, such as reflection or cancellation lemmas. Unfortunately
there is currently no easy way to tell Coq to use different defaults for
definitions and lemmas, so MathComp sticks to the on-demand default, as there
are significantly more lemmas than definition, and use the Prenex Implicits to
redress matters in bulk for definitions. However, this is not completely
systematic, and is sometimes omitted for constants that are not used as
functional arguments in the library, or inside the sections in which the
definition occur, since such commands need to be repeated after the section is
closed. Since Arguments commands should document the intended constant usage as
best as possible, they should follow the implicits policy - even in cases such
as this where the Prenex Implicits had been skipped.
Diffstat (limited to 'mathcomp')
35 files changed, 241 insertions, 250 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2501117..3fe8d01 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2663,7 +2663,7 @@ Coercion GLval ph (u : GLtype ph) : 'M[R]_n.-1.+1 := End FinUnitMatrix. Bind Scope group_scope with GLtype. -Arguments GLval {_%N _ _} _%g. +Arguments GLval {n%N R ph} u%g. Notation "{ ''GL_' n [ R ] }" := (GLtype n (Phant R)) (at level 0, n at level 2, format "{ ''GL_' n [ R ] }") : type_scope. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index af18125..c23d91c 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -216,9 +216,9 @@ Definition pinvmx : 'M_(n, m) := End Defs. -Arguments mxrank _%N _%N _%MS. +Arguments mxrank {m%N n%N} A%MS. Local Notation "\rank A" := (mxrank A) : nat_scope. -Arguments complmx _%N _%N _%MS. +Arguments complmx {m%N n%N} A%MS. Local Notation "A ^C" := (complmx A) : matrix_set_scope. Definition submx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => @@ -227,21 +227,21 @@ Fact submx_key : unit. Proof. by []. Qed. Definition submx := locked_with submx_key submx_def. Canonical submx_unlockable := [unlockable fun submx]. -Arguments submx {_%N _%N _%N} _%MS _%MS. +Arguments submx {m1%N m2%N n%N} A%MS B%MS : rename. Local Notation "A <= B" := (submx A B) : matrix_set_scope. Local Notation "A <= B <= C" := ((A <= B) && (B <= C))%MS : matrix_set_scope. Local Notation "A == B" := (A <= B <= A)%MS : matrix_set_scope. Definition ltmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) := (A <= B)%MS && ~~ (B <= A)%MS. -Arguments ltmx {_%N _%N _%N} _%MS _%MS. +Arguments ltmx {m1%N m2%N n%N} A%MS B%MS. Local Notation "A < B" := (ltmx A B) : matrix_set_scope. Definition eqmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) := prod (\rank A = \rank B) (forall m3 (C : 'M_(m3, n)), ((A <= C) = (B <= C)) * ((C <= A) = (C <= B)))%MS. -Arguments eqmx _%N _%N _%N _%MS _%MS. +Arguments eqmx {m1%N m2%N n%N} A%MS B%MS. Local Notation "A :=: B" := (eqmx A B) : matrix_set_scope. Section LtmxIdentities. @@ -296,7 +296,7 @@ Definition addsmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact addsmx_key : unit. Proof. by []. Qed. Definition addsmx := locked_with addsmx_key addsmx_def. Canonical addsmx_unlockable := [unlockable fun addsmx]. -Arguments addsmx {_%N _%N _%N} _%MS _%MS. +Arguments addsmx {m1%N m2%N n%N} A%MS B%MS : rename. Local Notation "A + B" := (addsmx A B) : matrix_set_scope. Local Notation "\sum_ ( i | P ) B" := (\big[addsmx/0]_(i | P) B%MS) : matrix_set_scope. @@ -330,8 +330,7 @@ Definition capmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact capmx_key : unit. Proof. by []. Qed. Definition capmx := locked_with capmx_key capmx_def. Canonical capmx_unlockable := [unlockable fun capmx]. -Arguments capmx _%N _%N _%N _%MS _%MS. -Prenex Implicits capmx. +Arguments capmx {m1%N m2%N n%N} A%MS B%MS : rename. Local Notation "A :&: B" := (capmx A B) : matrix_set_scope. Local Notation "\bigcap_ ( i | P ) B" := (\big[capmx/1%:M]_(i | P) B) : matrix_set_scope. @@ -341,7 +340,7 @@ Definition diffmx_def := idfun (fun m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) => Fact diffmx_key : unit. Proof. by []. Qed. Definition diffmx := locked_with diffmx_key diffmx_def. Canonical diffmx_unlockable := [unlockable fun diffmx]. -Arguments diffmx {_%N _%N _%N} _%MS _%MS. +Arguments diffmx {m1%N m2%N n%N} A%MS B%MS : rename. Local Notation "A :\: B" := (diffmx A B) : matrix_set_scope. Definition proj_mx n (U V : 'M_n) : 'M_n := pinvmx (col_mx U V) *m col_mx U 0. @@ -1725,7 +1724,7 @@ Inductive mxsum_spec n : forall m, 'M[F]_(m, n) -> nat -> Prop := | ProperMxsum m1 m2 T1 T2 r1 r2 of @mxsum_spec n m1 T1 r1 & @mxsum_spec n m2 T2 r2 : mxsum_spec (T1 + T2)%MS (r1 + r2)%N. -Arguments mxsum_spec _%N _%N _%MS _%N. +Arguments mxsum_spec {n%N m%N} T%MS r%N. Structure mxsum_expr m n := Mxsum { mxsum_val :> wrapped 'M_(m, n); @@ -1995,16 +1994,16 @@ Arguments mxdirect_sumsE {F I P n S_}. Arguments eigenspaceP {F n g a m W}. Arguments eigenvalueP {F n g a}. -Arguments mxrank {_ _%N _%N} _%MS. -Arguments complmx {_ _%N _%N} _%MS. -Arguments row_full _ _%N _%N _%MS. -Arguments submx {_ _%N _%N _%N} _%MS _%MS. -Arguments ltmx {_ _%N _%N _%N} _%MS _%MS. -Arguments eqmx {_ _%N _%N _%N} _%MS _%MS. -Arguments addsmx {_ _%N _%N _%N} _%MS _%MS. -Arguments capmx {_ _%N _%N _%N} _%MS _%MS. -Arguments diffmx _ _%N _%N _%N _%MS _%MS. -Prenex Implicits genmx. +Arguments mxrank {F m%N n%N} A%MS. +Arguments complmx {F m%N n%N} A%MS. +Arguments row_full {F m%N n%N} A%MS. +Arguments submx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments ltmx {F m1%N m2%N n%N} A%MS B%MS. +Arguments eqmx {F m1%N m2%N n%N} A%MS B%MS. +Arguments addsmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments capmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments diffmx {F m1%N m2%N n%N} A%MS B%MS : rename. +Arguments genmx {F m%N n%N} A%R : rename. Notation "\rank A" := (mxrank A) : nat_scope. Notation "<< A >>" := (genmx A) : matrix_set_scope. Notation "A ^C" := (complmx A) : matrix_set_scope. @@ -2279,7 +2278,7 @@ Qed. Definition mulsmx m1 m2 n (R1 : 'A[F]_(m1, n)) (R2 : 'A_(m2, n)) := (\sum_i <<R1 *m lin_mx (mulmxr (vec_mx (row i R2)))>>)%MS. -Arguments mulsmx _%N _%N _%N _%MS _%MS. +Arguments mulsmx {m1%N m2%N n%N} R1%MS R2%MS. Local Notation "R1 * R2" := (mulsmx R1 R2) : matrix_set_scope. @@ -2589,15 +2588,15 @@ Qed. End MatrixAlgebra. -Arguments mulsmx {_ _%N _%N _%N} _%MS _%MS. -Arguments left_mx_ideal _ _%N _%N _%N _%MS _%MS. -Arguments right_mx_ideal _ _%N _%N _%N _%MS _%MS. -Arguments mx_ideal _ _%N _%N _%N _%MS _%MS. -Arguments mxring_id _ _%N _%N _%R _%MS. -Arguments has_mxring_id _ _%N _%N _%R _%MS : extra scopes. -Arguments mxring _ _%N _%N _%MS. -Arguments cent_mx _ _%N _%N _%MS. -Arguments center_mx _ _%N _%N _%MS. +Arguments mulsmx {F m1%N m2%N n%N} R1%MS R2%MS. +Arguments left_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments right_mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments mx_ideal {F m1%N m2%N n%N} R%MS S%MS : rename. +Arguments mxring_id {F m%N n%N} R%MS e%R. +Arguments has_mxring_id {F m%N n%N} R%MS. +Arguments mxring {F m%N n%N} R%MS. +Arguments cent_mx {F m%N n%N} R%MS. +Arguments center_mx {F m%N n%N} R%MS. Notation "A \in R" := (submx (mxvec A) R) : matrix_set_scope. Notation "R * S" := (mulsmx R S) : matrix_set_scope. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 34174bf..929c313 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -146,9 +146,9 @@ End Polynomial. (* directives take effect. *) Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. -Arguments polyseq _ _%R. -Arguments poly_inj _ _%R _%R _. -Arguments coefp_head _ _ _%N _%R. +Arguments polyseq {R} p%R. +Arguments poly_inj {R} [p1%R p2%R] : rename. +Arguments coefp_head {R} h i%N p%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). Notation coefp i := (coefp_head tt i). @@ -2430,7 +2430,7 @@ Qed. End MapFieldPoly. -Arguments map_poly_inj {F R} f [x1 x2]. +Arguments map_poly_inj {F R} f [p1 p2] : rename. Section MaxRoots. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 854335d..4008f1a 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -3727,23 +3727,23 @@ End TermDef. Bind Scope term_scope with term. Bind Scope term_scope with formula. -Arguments Add {_} _%T _%T. -Arguments Opp {_} _%T. -Arguments NatMul {_} _%T _%N. -Arguments Mul {_} _%T _%T. -Arguments Inv {_} _%T. -Arguments Exp {_} _%T _%N. -Arguments Equal {_} _%T _%T. -Arguments Unit {_} _%T. -Arguments And {_} _%T _%T. -Arguments Or {_} _%T _%T. -Arguments Implies {_} _%T _%T. -Arguments Not {_} _%T. -Arguments Exists {_} _%N _%T. -Arguments Forall {_} _%N _%T. - -Arguments Bool {R}. -Arguments Const {R}. +Arguments Add {R} t1%T t2%T. +Arguments Opp {R} t1%T. +Arguments NatMul {R} t1%T n%N. +Arguments Mul {R} t1%T t2%T. +Arguments Inv {R} t1%T. +Arguments Exp {R} t1%T n%N. +Arguments Equal {R} t1%T t2%T. +Arguments Unit {R} t1%T. +Arguments And {R} f1%T f2%T. +Arguments Or {R} f1%T f2%T. +Arguments Implies {R} f1%T f2%T. +Arguments Not {R} f1%T. +Arguments Exists {R} i%N f1%T. +Arguments Forall {R} i%N f1%T. + +Arguments Bool {R} b. +Arguments Const {R} x. Notation True := (Bool true). Notation False := (Bool false). diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index d0214dd..614fbc2 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -369,7 +369,7 @@ Canonical int_countIdomainType := [countIdomainType of int]. Definition absz m := match m with Posz p => p | Negz n => n.+1 end. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. -Arguments absz _%distn_scope. +Arguments absz m%distn_scope. Local Notation "`| m |" := (absz m) : nat_scope. Module intOrdered. @@ -1607,7 +1607,7 @@ Module Export IntDist. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. -Arguments absz _%distn_scope. +Arguments absz m%distn_scope. Notation "`| m |" := (absz m) : nat_scope. Coercion Posz : nat >-> int. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index aef9a9f..542f8ad 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -245,7 +245,7 @@ Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A. Canonical hom_subType := [newType for f2mx]. End Hom. -Arguments mx2vs _ _ _%N _%MS. +Arguments mx2vs {K vT m%N} A%MS. Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx. End InternalTheory. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 6752623..a657fa5 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -544,7 +544,7 @@ Notation xcfun_r A := (xcfun_r_head tt A). Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope. Definition pred_Nirr gT B := #|@classes gT B|.-1. -Arguments pred_Nirr _ _%g. +Arguments pred_Nirr {gT} B%g. Notation Nirr G := (pred_Nirr G).+1. Notation Iirr G := 'I_(Nirr G). @@ -587,7 +587,7 @@ Proof. by apply: onW_bij; exists irr_of_socle. Qed. End IrrClassDef. Prenex Implicits socle_of_IirrK irr_of_socleK. -Arguments socle_of_Iirr _ _%R. +Arguments socle_of_Iirr {gT G%G} i%R. Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i)) (at level 8, i at level 2, format "''Chi_' i"). @@ -598,7 +598,7 @@ Definition irr_def gT B : (Nirr B).-tuple 'CF(B) := [tuple of mkseq irr_of (Nirr B)]. Definition irr := locked_with irr_key irr_def. -Arguments irr _ _%g. +Arguments irr {gT} B%g. Notation "''chi_' i" := (tnth (irr _) i%R) (at level 8, i at level 2, format "''chi_' i") : ring_scope. @@ -621,7 +621,7 @@ Proof. by move/Iirr1_neq0; exists (inord 1). Qed. Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i. Proof. -rewrite [irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG. +rewrite [@irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG. by rewrite cfRes_id inord_val. Qed. @@ -816,7 +816,7 @@ Qed. End IrrClass. -Arguments cfReg _ _%g. +Arguments cfReg {gT} B%g. Prenex Implicits cfIirr. Arguments irr_inj {gT G} [x1 x2]. @@ -1334,7 +1334,7 @@ Qed. End OrthogonalityRelations. -Arguments character_table _ _%g. +Arguments character_table {gT} G%g. Section InnerProduct. @@ -1565,7 +1565,7 @@ Qed. End IrrConstt. -Arguments irr_constt _ _%g _%CF. +Arguments irr_constt {gT B%g} phi%CF. Section Kernel. @@ -1733,7 +1733,7 @@ Qed. End Restrict. -Arguments Res_Iirr _ _%g _%g _%R. +Arguments Res_Iirr {gT A%g} B%g i%R. Section MoreConstt. @@ -1870,7 +1870,7 @@ Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed. End Isom. -Arguments isom_Iirr_inj [aT rT G f R] isoGR [x1 x2]. +Arguments isom_Iirr_inj {aT rT G f R} isoGR [i1 i2] : rename. Section IsomInv. @@ -1938,7 +1938,7 @@ Qed. End Sdprod. -Arguments sdprod_Iirr_inj [gT K H G] defG [x1 x2]. +Arguments sdprod_Iirr_inj {gT K H G} defG [i1 i2] : rename. Section DProd. @@ -2089,7 +2089,7 @@ Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed. End DProd. -Arguments dprod_Iirr_inj [gT G K H] KxH [x1 x2]. +Arguments dprod_Iirr_inj {gT G K H} KxH [i1 i2] : rename. 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. -Arguments aut_Iirr_inj [gT G] u [x1 x2]. +Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename. Section Coset. @@ -2993,4 +2993,4 @@ Proof. by move/cfker_Ind->; rewrite ?irr_neq0 ?irr_char. Qed. End Induced. -Arguments Ind_Iirr _ _%g _%g _%R.
\ No newline at end of file +Arguments Ind_Iirr {gT A%g} B%g i%R. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index ac3e5bc..7b2b90d 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -392,14 +392,13 @@ End Defs. Bind Scope cfun_scope with classfun. -Arguments classfun _ _%g. -Arguments classfun_on _ _%g _%g. -Arguments cfun_indicator _ _%g. -Arguments cfAut _ _%g _ _%CF. -Arguments cfReal _ _%g _%CF. -Arguments cfdot _ _%g _%CF _%CF. -Arguments cfdotr_head _ _%g _ _%CF _%CF. -Arguments cfdotr_head _ _%g _ _%CF. +Arguments classfun {gT} B%g. +Arguments classfun_on {gT} B%g A%g. +Arguments cfun_indicator {gT} B%g. +Arguments cfAut {gT B%g} u phi%CF. +Arguments cfReal {gT B%g} phi%CF. +Arguments cfdot {gT B%g} phi%CF psi%CF. +Arguments cfdotr_head {gT B%g} k psi%CF phi%CF. Notation "''CF' ( G )" := (classfun G) : type_scope. Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope. @@ -452,12 +451,12 @@ End Predicates. (* Outside section so the nosimpl does not get "cooked" out. *) Definition orthogonal gT D S1 S2 := nosimpl (@ortho_rec gT D S1 S2). -Arguments cfker _ _%g _%CF. -Arguments cfaithful _ _%g _%CF. -Arguments orthogonal _ _%g _%CF _%CF. -Arguments pairwise_orthogonal _ _%g _%CF. -Arguments orthonormal _ _%g _%CF. -Arguments isometry _ _ _%g _%g _%CF. +Arguments cfker {gT D%g} phi%CF. +Arguments cfaithful {gT D%g} phi%CF. +Arguments orthogonal {gT D%g} S1%CF S2%CF. +Arguments pairwise_orthogonal {gT D%g} S%CF. +Arguments orthonormal {gT D%g} S%CF. +Arguments isometry {gT rT D%g R%g} tau%CF. Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" := (isometry_from_to (mem CFD) tau (mem CFR)) @@ -756,7 +755,7 @@ Proof. by []. Qed. End ClassFun. -Arguments classfun_on _ _%g _%g. +Arguments classfun_on {gT} B%g A%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Arguments cfun_onP {gT G A phi}. @@ -1394,7 +1393,7 @@ Canonical cfRes_lrmorphism := [lrmorphism of cfRes]. End Restrict. -Arguments cfRes _ _%g _%g _%CF. +Arguments cfRes {gT} A%g {B%g} phi%CF. Notation "''Res[' H , G ]" := (@cfRes _ H G) (only parsing) : ring_scope. Notation "''Res[' H ]" := 'Res[H, _] : ring_scope. Notation "''Res'" := 'Res[_] (only parsing) : ring_scope. @@ -1621,7 +1620,7 @@ Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed. End InvMorphism. -Arguments cfIsom_inj [aT rT G f R] isoGR [x1 x2]. +Arguments cfIsom_inj {aT rT G f R} isoGR [phi1 phi2] : rename. Section Coset. @@ -1727,9 +1726,8 @@ Proof. by move=> nsBG kerH; rewrite -cfMod_eq1 // cfQuoK. Qed. End Coset. -Arguments cfQuo _ _%G _%g _%CF. -Arguments cfMod _ _%G _%g _%CF. -Prenex Implicits cfMod. +Arguments cfQuo {gT G%G} B%g phi%CF. +Arguments cfMod {gT G%G B%g} phi%CF. Notation "phi / H" := (cfQuo H phi) : cfun_scope. Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope. @@ -2327,7 +2325,7 @@ Qed. End Induced. -Arguments cfInd _ _%g _%g _%CF. +Arguments cfInd {gT} B%g {A%g} phi%CF. Notation "''Ind[' G , H ]" := (@cfInd _ G H) (only parsing) : ring_scope. Notation "''Ind[' G ]" := 'Ind[G, _] : ring_scope. Notation "''Ind'" := 'Ind[_] (only parsing) : ring_scope. @@ -2489,7 +2487,7 @@ End FieldAutomorphism. Arguments cfAutK u {gT G}. Arguments cfAutVK u {gT G}. -Arguments cfAut_inj u [gT G x1 x2]. +Arguments cfAut_inj u {gT G} [phi1 phi2] : rename. Definition conj_cfRes := cfAutRes conjC. Definition cfker_conjC := cfker_aut conjC. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index ffa9696..80d5cc5 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -567,9 +567,9 @@ Qed. End Inertia. -Arguments inertia _ _%g _%CF. -Arguments cfclass _ _%g _%CF _%g. -Arguments conjg_Iirr_inj [gT H] y [x1 x2]. +Arguments inertia {gT B%g} phi%CF. +Arguments cfclass {gT A%g} phi%CF B%g. +Arguments conjg_Iirr_inj {gT H} y [i1 i2] : rename. Notation "''I[' phi ] " := (inertia phi) : group_scope. Notation "''I[' phi ] " := (inertia_group phi) : Group_scope. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index f0553f2..3c2b0d6 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -157,7 +157,7 @@ Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode]. End GenericClassSums. -Arguments gring_irr_mode _ _%G _%R _%g : extra scopes. +Arguments gring_irr_mode {gT G%G} i%R _%g : extra scopes. Notation "''K_' i" := (gring_class_sum _ i) (at level 8, i at level 2, format "''K_' i") : ring_scope. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index b121f4c..69055d4 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -341,7 +341,7 @@ Proof. by move=> sHG; rewrite gacentE // setTI afix_repr. Qed. End FinFieldRepr. -Arguments rowg_mx _ _ _%g. +Arguments rowg_mx {F n%N} L%g. Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope. Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope. @@ -406,7 +406,7 @@ Open Scope abelem_scope. Definition abelem_dim' (gT : finGroupType) (E : {set gT}) := (logn (pdiv #|E|) #|E|).-1. -Arguments abelem_dim' _ _%g. +Arguments abelem_dim' {gT} E%g. Notation "''dim' E" := (abelem_dim' E).+1 (at level 10, E at level 8, format "''dim' E") : abelem_scope. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 6859168..560b61d 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -814,10 +814,10 @@ End Regular. End RingRepr. -Arguments mx_representation _ _ _%g _%N. -Arguments mx_repr _ _ _%g _%N _. -Arguments group_ring _ _ _%g. -Arguments regular_repr _ _ _%g. +Arguments mx_representation R {gT} G%g n%N. +Arguments mx_repr {R gT} G%g {n%N} r. +Arguments group_ring R {gT} G%g. +Arguments regular_repr R {gT} G%g. Arguments centgmxP {R gT G n rG f}. Arguments rkerP {R gT G n rG x}. @@ -2377,8 +2377,8 @@ 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}. -Arguments val_submod_inj {n U m}. -Arguments val_factmod_inj {n U m}. +Arguments val_submod_inj {n U m} [W1 W2] : rename. +Arguments val_factmod_inj {n U m} [W1 W2] : rename. Section Proper. @@ -4652,10 +4652,10 @@ End LinearIrr. End FieldRepr. -Arguments rfix_mx _ _ _%g _%N _ _%g. -Arguments gset_mx _ _ _%g _%g. -Arguments classg_base _ _ _%g _%g : extra scopes. -Arguments irrType _ _ _%g _%g : extra scopes. +Arguments rfix_mx {F gT G%g n%N} rG H%g. +Arguments gset_mx F {gT} G%g A%g. +Arguments classg_base F {gT} G%g _%g : extra scopes. +Arguments irrType F {gT} G%g. Arguments mxmoduleP {F gT G n rG m U}. Arguments envelop_mxP {F gT G n rG A}. @@ -4671,16 +4671,16 @@ 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}. +Arguments val_submod_inj {F n U m} [W1 W2] : rename. +Arguments val_factmod_inj {F n U m} [W1 W2] : rename. Notation "'Cl" := (Clifford_action _) : action_scope. Bind Scope irrType_scope with socle_sort. Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope. -Arguments irr_degree _ _ _%G _ _%irr. -Arguments irr_repr _ _ _%G _ _%irr _%g : extra scopes. -Arguments irr_mode _ _ _%G _ _%irr _%g : extra scopes. +Arguments irr_degree {F gT G%G sG} i%irr. +Arguments irr_repr [F gT G%G sG] i%irr _%g : extra scopes. +Arguments irr_mode [F gT G%G sG] i%irr z%g : rename. Notation "''n_' i" := (irr_degree i) : group_ring_scope. Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope. Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 8a65f2b..ad2388a 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. -Arguments map_poly_inj {F R} f [x1 x2]. +Arguments map_poly_inj {F R} f [p1 p2]. Theorem Fundamental_Theorem_of_Algebraics : {L : closedFieldType & diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 1ae025b..0440653 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -54,18 +54,18 @@ Proof. by split=> /andP[]. Qed. Notation cps T := ((T -> fF) -> fF). Definition ret T1 : T1 -> cps T1 := fun x k => k x. -Arguments ret T1 x k /. +Arguments ret {T1} x k /. Definition bind T1 T2 (x : cps T1) (f : T1 -> cps T2) : cps T2 := fun k => x (fun x => f x k). -Arguments bind T1 T2 x f k /. +Arguments bind {T1 T2} x f k /. Notation "''let' x <- y ; z" := (bind y (fun x => z)) (at level 99, x at level 0, y at level 0, format "'[hv' ''let' x <- y ; '/' z ']'"). Definition cpsif T (c : fF) (t : T) (e : T) : cps T := fun k => GRing.If c (k t) (k e). -Arguments cpsif T c t e k /. +Arguments cpsif {T} c t e k /. Notation "''if' c1 'then' c2 'else' c3" := (cpsif c1%T c2%T c3%T) (at level 200, right associativity, format "'[hv ' ''if' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'"). diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 0410e55..7e86d3c 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -620,8 +620,8 @@ End FalgebraTheory. Delimit Scope aspace_scope with AS. Bind Scope aspace_scope with aspace. Bind Scope aspace_scope with aspace_of. -Arguments asval _ _ _%AS. -Arguments clone_aspace _ _ _%VS _%AS _ _. +Arguments asval {K aT} a%AS. +Arguments clone_aspace [K aT U%VS A%AS algU] _. Notation "{ 'aspace' T }" := (aspace_of (Phant T)) : type_scope. Notation "A * B" := (prodv A B) : vspace_scope. diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index ffea847..9a8032d 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -148,10 +148,10 @@ End ActionDef. (* Need to close the Section here to avoid re-declaring all Argument Scopes *) Delimit Scope action_scope with act. Bind Scope action_scope with action. -Arguments act_morph _ _%g _ _ _%g : extra scopes. -Arguments is_action _ _%g _ _. -Arguments act _ _%g _%type _%act _%g _%g. -Arguments clone_action _ _%g _%type _%act _. +Arguments act_morph {aT rT%type} to x%g. +Arguments is_action {aT} D%g {rT} to. +Arguments act {aT D%g rT%type} to%act x%g a%g : rename. +Arguments clone_action [aT D%g rT%type to%act] _. Notation "{ 'action' aT &-> T }" := (action [set: aT] T) (at level 0, format "{ 'action' aT &-> T }") : type_scope. @@ -210,15 +210,15 @@ Definition faithful A S to := A :&: astab S to \subset [1]. End ActionDefs. -Arguments setact _ _%g _ _%act _%g _%g. -Arguments orbit _ _%g _ _%act _%g _%g. -Arguments amove _ _%g _ _%act _%g _%g _%g. -Arguments afix _ _%g _ _%act _%g. -Arguments astab _ _%g _ _%g _%act. -Arguments astabs _ _%g _ _%g _%act. -Arguments acts_on _ _%g _ _%g _%g _%act. -Arguments atrans _ _%g _ _%g _%g _%act. -Arguments faithful _ _%g _ _%g _%g _%act. +Arguments setact {aT D%g rT} to%act S%g a%g. +Arguments orbit {aT D%g rT} to%act A%g x%g. +Arguments amove {aT D%g rT} to%act A%g x%g y%g. +Arguments afix {aT D%g rT} to%act A%g. +Arguments astab {aT D%g rT} S%g to%act. +Arguments astabs {aT D%g rT} S%g to%act. +Arguments acts_on {aT D%g rT} A%g S%g to%act. +Arguments atrans {aT D%g rT} A%g S%g to%act. +Arguments faithful {aT D%g rT} A%g S%g to%act. Notation "to ^*" := (setact to) (at level 2, format "to ^*") : fun_scope. @@ -482,9 +482,7 @@ End Reindex. End RawAction. -(* Warning: this directive depends on names of bound variables in the *) -(* definition of injective, in ssrfun.v. *) -Arguments act_inj {aT D rT} to _ [x1 x2]. +Arguments act_inj {aT D rT} to a [x1 x2] : rename. Notation "to ^*" := (set_action to) : action_scope. @@ -874,7 +872,7 @@ Qed. End PartialAction. -Arguments orbit_transversal _ _%g _ _%act _%g _%g. +Arguments orbit_transversal {aT D%g rT} to%act A%g S%g. 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]. @@ -1741,7 +1739,7 @@ Qed. End AutIn. -Arguments Aut_in _ _%g _%g. +Arguments Aut_in {gT} A%g B%g. Section InjmAutIn. @@ -1818,9 +1816,9 @@ End GroupAction. Delimit Scope groupAction_scope with gact. Bind Scope groupAction_scope with groupAction. -Arguments is_groupAction _ _ _%g _%g _%act. -Arguments groupAction _ _ _%g _%g. -Arguments gact _ _ _%g _%g _%gact. +Arguments is_groupAction {aT rT D%g} R%g to%act. +Arguments groupAction {aT rT} D%g R%g. +Arguments gact {aT rT D%g R%g} to%gact : rename. Notation "[ 'groupAction' 'of' to ]" := (clone_groupAction (@GroupAction _ _ _ _ to)) @@ -1847,9 +1845,9 @@ Definition acts_irreducibly A S to := End GroupActionDefs. -Arguments gacent _ _ _%g _%g _%gact _%g. -Arguments acts_on_group _ _ _%g _%g _%g _%g _%gact. -Arguments acts_irreducibly _ _ _%g _%g _%g _%g _%gact. +Arguments gacent {aT rT D%g R%g} to%gact A%g. +Arguments acts_on_group {aT rT D%g R%g} A%g S%g to%gact. +Arguments acts_irreducibly {aT rT D%g R%g} A%g S%g to%gact. Notation "''C_' ( | to ) ( A )" := (gacent to A) (at level 8, format "''C_' ( | to ) ( A )") : group_scope. @@ -2705,8 +2703,8 @@ Canonical aut_groupAction := GroupAction autact_is_groupAction. End AutAct. -Arguments aut_action _ _%g. -Arguments aut_groupAction _ _%g. +Arguments aut_action {gT} G%g. +Arguments aut_groupAction {gT} G%g. Notation "[ 'Aut' G ]" := (aut_action G) : action_scope. Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 1165a33..a68bc9f 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -493,7 +493,7 @@ Qed. End PreGroupIdentities. Hint Resolve commute1. -Arguments invg_inj {T}. +Arguments invg_inj {T} [x1 x2]. Prenex Implicits commute invgK. Section GroupIdentities. @@ -643,7 +643,7 @@ Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))). Arguments mulgI [T]. Arguments mulIg [T]. -Arguments conjg_inj [T]. +Arguments conjg_inj {T} x [x1 x2]. Arguments commgP {T x y}. Arguments conjg_fixP {T x y}. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 322fc4e..97b2eba 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -750,8 +750,8 @@ Qed. End EqIso. -Arguments qisom_inj [gT G H]. -Arguments morphim_qisom_inj [gT G H]. +Arguments qisom_inj {gT G H} eqGH [x1 x2]. +Arguments morphim_qisom_inj {gT G H} eqGH [x1 x2]. Section FirstIsomorphism. diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 5f1a013..746898f 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -111,16 +111,16 @@ Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|. End AbelianDefs. -Arguments exponent _ _%g. -Arguments abelem _ _%N _%g. -Arguments is_abelem _ _%g. -Arguments pElem _ _%N _%g. -Arguments pnElem _ _%N _%N _%g. -Arguments nElem _ _%N _%g. -Arguments pmaxElem _ _%N _%g. -Arguments p_rank _ _%N _%g. -Arguments rank _ _%g. -Arguments gen_rank _ _%g. +Arguments exponent {gT} A%g. +Arguments abelem {gT} p%N A%g. +Arguments is_abelem {gT} A%g. +Arguments pElem {gT} p%N A%g. +Arguments pnElem {gT} p%N n%N A%g. +Arguments nElem {gT} n%N A%g. +Arguments pmaxElem {gT} p%N A%g. +Arguments p_rank {gT} p%N A%g. +Arguments rank {gT} A%g. +Arguments gen_rank {gT} A%g. Notation "''Ldiv_' n ()" := (Ldiv _ n) (at level 8, n at level 2, format "''Ldiv_' n ()") : group_scope. @@ -192,10 +192,10 @@ Qed. End Functors. -Arguments Ohm _%N _ _%g. -Arguments Ohm_group _%N _ _%g. -Arguments Mho _%N _ _%g. -Arguments Mho_group _%N _ _%g. +Arguments Ohm n%N {gT} A%g. +Arguments Ohm_group n%N {gT} A%g. +Arguments Mho n%N {gT} A%g. +Arguments Mho_group n%N {gT} A%g. Arguments OhmPredP {n gT x}. Notation "''Ohm_' n ( G )" := (Ohm n G) @@ -2023,8 +2023,8 @@ Qed. End AbelianStructure. -Arguments abelian_type {_} _%g. -Arguments homocyclic {_} _%g. +Arguments abelian_type {gT} A%g. +Arguments homocyclic {gT} A%g. Section IsogAbelian. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 1c804cc..10cbbaa 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. -Arguments burnside_formula [gT]. +Arguments burnside_formula {gT}. Section colouring. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 98434ba..88774db 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -56,11 +56,11 @@ Canonical center_group (G : {group gT}) : {group gT} := End Defs. -Arguments center _ _%g. +Arguments center {gT} A%g. Notation "''Z' ( A )" := (center A) : group_scope. Notation "''Z' ( H )" := (center_group H) : Group_scope. -Lemma morphim_center : GFunctor.pcontinuous center. +Lemma morphim_center : GFunctor.pcontinuous (@center). Proof. by move=> gT rT G D f; apply: morphim_subcent. Qed. Canonical center_igFun := [igFun by fun _ _ => subsetIl _ _ & morphim_center]. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index dcd53ce..7895116 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -33,7 +33,7 @@ Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) := (* "cooking" destroys it. *) Definition derived_at := nosimpl derived_at_rec. -Arguments derived_at _%N _ _%g. +Arguments derived_at n%N {gT} A%g. Notation "G ^` ( n )" := (derived_at n G) : group_scope. Section DerivedBasics. @@ -354,7 +354,7 @@ End Commutator_properties. Arguments derG1P {gT G}. -Lemma der_cont n : GFunctor.continuous (derived_at n). +Lemma der_cont n : GFunctor.continuous (@derived_at n). Proof. by move=> aT rT G f; rewrite morphim_der. Qed. Canonical der_igFun n := [igFun by der_sub^~ n & der_cont n]. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 046f4a2..e370a7e 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -289,9 +289,9 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed. End Cyclic. -Arguments cyclic {_} _%g. -Arguments generator {_}_%g _%g. -Arguments expg_invn {_} _%g _%N. +Arguments cyclic {gT} A%g. +Arguments generator {gT} A%g a%g. +Arguments expg_invn {gT} A%g k%N. Arguments cyclicP {gT A}. Prenex Implicits cyclic Zpm. @@ -556,7 +556,7 @@ Qed. End Metacyclic. -Arguments metacyclic {_} _%g. +Arguments metacyclic {gT} A%g. Arguments metacyclicP {gT A}. (* Automorphisms of cyclic groups. *) diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index f7edfc9..01ba8f3 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -98,15 +98,15 @@ Variant has_Frobenius_action G H : Prop := End Definitions. -Arguments semiregular _ _%g _%g. -Arguments semiprime _ _%g _%g. -Arguments normedTI _ _%g _%g _%g. -Arguments Frobenius_group_with_complement _ _%g _%g. -Arguments Frobenius_group _ _%g. -Arguments Frobenius_group_with_kernel _ _%g _%g. -Arguments Frobenius_group_with_kernel_and_complement _ _%g _%g _%g. -Arguments Frobenius_action _ _%g _%g _ _%g _%act. -Arguments has_Frobenius_action _ _%g _%g. +Arguments semiregular {gT} K%g H%g. +Arguments semiprime {gT} K%g H%g. +Arguments normedTI {gT} A%g G%g L%g. +Arguments Frobenius_group_with_complement {gT} G%g H%g. +Arguments Frobenius_group {gT} G%g. +Arguments Frobenius_group_with_kernel {gT} G%g K%g. +Arguments Frobenius_group_with_kernel_and_complement {gT} G%g K%g H%g. +Arguments Frobenius_action {gT} G%g H%g {sT} S%g to%act. +Arguments has_Frobenius_action {gT} G%g H%g. Notation "[ 'Frobenius' G 'with' 'complement' H ]" := (Frobenius_group_with_complement G H) diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index a1830b9..3e99bfb 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -71,16 +71,16 @@ Definition simple A := minnormal A A. Definition chief_factor A V U := maxnormal V U A && (U <| A). End GroupDefs. -Arguments subnormal {_} _%g _%g. -Arguments invariant_factor _ _%g _%g _%g. -Arguments stable_factor _ _%g _%g _%g. -Arguments central_factor _ _%g _%g _%g. -Arguments maximal {_} _%g _%g. -Arguments maximal_eq _ _%g _%g. -Arguments maxnormal _ _%g _%g _%g. -Arguments minnormal _ _%g _%g. -Arguments simple {_} _%g. -Arguments chief_factor _ _%g _%g _%g. +Arguments subnormal {gT} A%g B%g. +Arguments invariant_factor {gT} A%g B%g C%g. +Arguments stable_factor {gT} A%g V%g U%g. +Arguments central_factor {gT} A%g V%g U%g. +Arguments maximal {gT} A%g B%g. +Arguments maximal_eq {gT} A%g B%g. +Arguments maxnormal {gT} A%g B%g U%g. +Arguments minnormal {gT} A%g B%g. +Arguments simple {gT} A%g. +Arguments chief_factor {gT} A%g V%g U%g. Notation "H <|<| G" := (subnormal H G) (at level 70, no associativity) : group_scope. @@ -94,7 +94,7 @@ Notation "A .-central" := (central_factor A) Notation "G .-chief" := (chief_factor G) (at level 2, format "G .-chief") : group_rel_scope. -Arguments group_rel_of _ _%group_rel_scope _%G _%G : extra scopes. +Arguments group_rel_of {gT} r%group_rel_scope _%G _%G : extra scopes. Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r))) (at level 2, format "r .-series") : group_scope. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 91cc709..bda66bd 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -475,8 +475,8 @@ Qed. End StableCompositionSeries. -Arguments maxainv _ _ _%G _%G _%gact _%g _%g. -Arguments asimple _ _ _%G _%G _%gact _%g. +Arguments maxainv {aT rT D%G A%G} to%gact B%g C%g. +Arguments asimple {aT rT D%G A%G} to%gact K%g. Section StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 5f7a9ed..781abbe 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -102,16 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)]. End Defs. -Arguments charsimple _ _%g. -Arguments Frattini _ _%g. -Arguments Fitting _ _%g. -Arguments critical _ _%g _%g. -Arguments special _ _%g. -Arguments extraspecial _ _%g. -Arguments SCN _ _%g. -Arguments SCN_at _ _%N _%g. - -Prenex Implicits maximal simple charsimple critical special extraspecial. +Arguments charsimple {gT} A%g. +Arguments Frattini {gT} A%g. +Arguments Fitting {gT} A%g. +Arguments critical {gT} A%g B%g. +Arguments special {gT} A%g. +Arguments extraspecial {gT} A%g. +Arguments SCN {gT} B%g. +Arguments SCN_at {gT} n%N B%g. Notation "''Phi' ( A )" := (Frattini A) (at level 8, format "''Phi' ( A )") : group_scope. @@ -459,7 +457,7 @@ Section FittingFun. Implicit Types gT rT : finGroupType. -Lemma morphim_Fitting : GFunctor.pcontinuous Fitting. +Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting). Proof. move=> gT rT G D f; apply: Fitting_max. by rewrite morphim_normal ?Fitting_normal. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index d631919..aee3113 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -52,8 +52,8 @@ Definition lower_central_at n := lower_central_at_rec n.-1. (* "cooking" destroys it. *) Definition upper_central_at := nosimpl upper_central_at_rec. -Arguments lower_central_at _%N _ _%g. -Arguments upper_central_at _%N _ _%g. +Arguments lower_central_at n%N {gT} A%g. +Arguments upper_central_at n%N {gT} A%g. Notation "''L_' n ( G )" := (lower_central_at n G) (at level 8, n at level 2, format "''L_' n ( G )") : group_scope. @@ -75,9 +75,9 @@ Definition solvable := End PropertiesDefs. -Arguments nilpotent {_} _%g. -Arguments nil_class {_} _%g. -Arguments solvable {_} _%g. +Arguments nilpotent {gT} A%g. +Arguments nil_class {gT} A%g. +Arguments solvable {gT} A%g. Section NilpotentProps. @@ -320,7 +320,7 @@ End LowerCentral. Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope. -Lemma lcn_cont n : GFunctor.continuous (lower_central_at n). +Lemma lcn_cont n : GFunctor.continuous (@lower_central_at n). Proof. case: n => //; elim=> // n IHn g0T h0T H phi. by rewrite !lcnSn morphimR ?lcn_sub // commSg ?IHn. @@ -338,7 +338,7 @@ Implicit Type gT : finGroupType. Lemma ucn_pmap : exists hZ : GFunctor.pmap, @upper_central_at n = hZ. Proof. elim: n => [|n' [hZ defZ]]; first by exists trivGfun_pgFun. -by exists [pgFun of center %% hZ]; rewrite /= -defZ. +by exists [pgFun of @center %% hZ]; rewrite /= -defZ. Qed. (* Now extract all the intermediate facts of the last proof. *) @@ -351,7 +351,7 @@ Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G). Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G. Proof. by have [hZ ->] := ucn_pmap; apply: gFsub. Qed. -Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n). +Lemma morphim_ucn : GFunctor.pcontinuous (@upper_central_at n). Proof. by have [hZ ->] := ucn_pmap; apply: pmorphimF. Qed. Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn]. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 6c02e7b..d62154f 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -83,15 +83,15 @@ Definition Sylow A B := p_group B && Hall A B. End PgroupDefs. -Arguments pgroup {_} _%N _%g. -Arguments psubgroup _ _%N _%g _%g. -Arguments p_group _ _%g. -Arguments p_elt _ _%N. -Arguments constt _ _%g _%N. -Arguments Hall {_} _%g _%g. -Arguments pHall _ _%N _%g _%g. -Arguments Syl _ _%N _%g. -Arguments Sylow {_} _%g _%g. +Arguments pgroup {gT} pi%N A%g. +Arguments psubgroup {gT} pi%N A%g B%g. +Arguments p_group {gT} A%g. +Arguments p_elt {gT} pi%N x. +Arguments constt {gT} x%g pi%N. +Arguments Hall {gT} A%g B%g. +Arguments pHall {gT} pi%N A%g B%g. +Arguments Syl {gT} p%N A%g. +Arguments Sylow {gT} A%g B%g. Notation "pi .-group" := (pgroup pi) (at level 2, format "pi .-group") : group_scope. @@ -861,8 +861,8 @@ Canonical pcore_group : {group gT} := Eval hnf in [group of pcore]. End PcoreDef. -Arguments pcore _ _%N _%g. -Arguments pcore_group _ _%N _%G. +Arguments pcore pi%N {gT} A%g. +Arguments pcore_group pi%N {gT} A%G. Notation "''O_' pi ( G )" := (pcore pi G) (at level 8, pi at level 2, format "''O_' pi ( G )") : group_scope. Notation "''O_' pi ( G )" := (pcore_group pi G) : Group_scope. @@ -884,7 +884,7 @@ Canonical pseries_group : {group gT} := group pseries_group_set. End PseriesDefs. -Arguments pseries _ _%SEQ _%g. +Arguments pseries pis%SEQ {gT} _%g. Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing). Notation "''O_{' p1 , .. , pn } ( A )" := (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A) @@ -977,7 +977,7 @@ Section MorphPcore. Implicit Types (pi : nat_pred) (gT rT : finGroupType). -Lemma morphim_pcore pi : GFunctor.pcontinuous (pcore pi). +Lemma morphim_pcore pi : GFunctor.pcontinuous (@pcore pi). Proof. move=> gT rT D G f; apply/bigcapsP=> M /normal_sub_max_pgroup; apply. by rewrite morphim_pgroup ?pcore_pgroup. @@ -1054,7 +1054,7 @@ Lemma pseries_rcons pi pis gT (A : {set gT}) : Proof. by rewrite /pseries rev_rcons. Qed. Lemma pseries_subfun pis : - GFunctor.closed (pseries pis) /\ GFunctor.pcontinuous (pseries pis). + GFunctor.closed (@pseries pis) /\ GFunctor.pcontinuous (@pseries pis). Proof. elim/last_ind: pis => [|pis pi [sFpi fFpi]]. by split=> [gT G | gT rT D G f]; rewrite (sub1G, morphim1). @@ -1064,13 +1064,13 @@ split=> [gT G | gT rT D G f]; rewrite !pseries_rcons ?(pcore_mod_sub F) //. exact: (morphim_pcore_mod F). Qed. -Lemma pseries_sub pis : GFunctor.closed (pseries pis). +Lemma pseries_sub pis : GFunctor.closed (@pseries pis). Proof. by case: (pseries_subfun pis). Qed. -Lemma morphim_pseries pis : GFunctor.pcontinuous (pseries pis). +Lemma morphim_pseries pis : GFunctor.pcontinuous (@pseries pis). Proof. by case: (pseries_subfun pis). Qed. -Lemma pseriesS pis : GFunctor.hereditary (pseries pis). +Lemma pseriesS pis : GFunctor.hereditary (@pseries pis). Proof. exact: (morphim_pseries pis). Qed. Canonical pseries_igFun pis := [igFun by pseries_sub pis & morphim_pseries pis]. @@ -1149,7 +1149,7 @@ apply: (quotient_inj nH2H). by apply/andP; rewrite /= -cats1 pseries_sub_catl pseries_norm2. rewrite /= quotient_pseries /= -IHpi -rcons_cat. rewrite -[G / _ / _](morphim_invm inj_f) //= {2}im_f //. -rewrite -(@injmF [igFun of pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries. +rewrite -(@injmF [igFun of @pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries. by rewrite -im_f ?morphim_invm ?morphimS ?normal_sub. Qed. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 58a5f20..fa27e75 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -43,14 +43,12 @@ Definition primitive := End PrimitiveDef. -Arguments imprimitivity_system _ _ _%g _%g _%act _%g. -Arguments primitive _ _ _%g _%g _%act. +Arguments imprimitivity_system {aT sT} A%g S%g to%act Q%g. +Arguments primitive {aT sT} A%g S%g to%act. Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to) (at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope. -Prenex Implicits imprimitivity_system. - Section Primitive. Variables (aT : finGroupType) (sT : finType). @@ -183,9 +181,9 @@ Qed. End NTransitive. -Arguments dtuple_on _ _%N _%g. -Arguments ntransitive _ _ _%N _%g _%g _%act. -Arguments n_act [gT sT] _ [n]. +Arguments dtuple_on {sT} n%N S%g. +Arguments ntransitive {gT sT} n%N A%g S%g to%act. +Arguments n_act {gT sT} to {n} t a. Notation "n .-dtuple ( S )" := (dtuple_on n S) (at level 8, format "n .-dtuple ( S )") : set_scope. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index f940ec9..a428c0d 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -535,7 +535,7 @@ Qed. End Zgroups. -Arguments Zgroup {_} _%g. +Arguments Zgroup {gT} A%g. Section NilPGroups. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 4487ab4..7473ed7 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -460,7 +460,7 @@ Notation "x |-> y" := (FunDelta x y) format "'[hv' x '/ ' |-> y ']'") : fun_delta_scope. Delimit Scope fun_delta_scope with FUN_DELTA. -Arguments app_fdelta _ _%type _%FUN_DELTA _ _. +Arguments app_fdelta {aT rT%type} df%FUN_DELTA f z. Notation "[ 'fun' z : T => F 'with' d1 , .. , dn ]" := (SimplFunDelta (fun z : T => @@ -603,7 +603,7 @@ 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}. +Arguments val_inj {T P sT} [x1 x2]. Prenex Implicits val insubd. Local Notation inlined_sub_rect := @@ -779,7 +779,7 @@ Proof. by case/andP. Qed. End ProdEqType. -Arguments pair_eq {T1 T2} _ _ /. +Arguments pair_eq {T1 T2} u v /. Arguments pair_eqP {T1 T2}. Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) := @@ -805,7 +805,7 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin. End OptionEqType. -Arguments opt_eq {T} !_ !_. +Arguments opt_eq {T} !u !v. Section TaggedAs. @@ -851,7 +851,7 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed. End TagEqType. -Arguments tag_eq {I T_} !_ !_. +Arguments tag_eq {I T_} !u !v. Arguments tag_eqP {I T_ x y}. Section SumEqType. @@ -875,5 +875,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed. End SumEqType. -Arguments sum_eq {T1 T2} !_ !_. +Arguments sum_eq {T1 T2} !u !v. Arguments sum_eqP {T1 T2 x y}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 3fd10fa..4ad02c6 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -130,7 +130,7 @@ Delimit Scope set_scope with SET. Bind Scope set_scope with set_type. Bind Scope set_scope with set_of. Open Scope set_scope. -Arguments finfun_of_set _ _%SET. +Arguments finfun_of_set {T} A%SET. Notation "{ 'set' T }" := (set_of (Phant T)) (at level 0, format "{ 'set' T }") : type_scope. @@ -955,7 +955,7 @@ Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed. End setOps. Arguments set1P {T x a}. -Arguments set1_inj {T}. +Arguments set1_inj {T} [x1 x2]. Arguments set2P {T x a b}. Arguments setIdP {T x pA pB}. Arguments setIP {T x A B}. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 4b2952f..d4f564f 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1760,7 +1760,7 @@ Qed. End EnumRank. -Arguments enum_val_inj {T A} [x1 x2]. +Arguments enum_val_inj {T A} [i1 i2] : rename. Arguments enum_rank_inj {T} [x1 x2]. Prenex Implicits enum_val enum_rank. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index b24da11..b8388f0 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. -Arguments eqn !_ !_. +Arguments eqn !m !n. Arguments eqnP {x y}. Lemma eqnE : eqn = eq_op. Proof. by []. Qed. @@ -1454,7 +1454,7 @@ Qed. Canonical bin_nat_eqMixin := EqMixin eq_binP. Canonical bin_nat_eqType := Eval hnf in EqType N bin_nat_eqMixin. -Arguments N.eqb !_ !_. +Arguments N.eqb !n !m. Section NumberInterpretation. |