diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index be469f5..9a0034d 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -1998,7 +1998,7 @@ 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 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_}. @@ -2619,7 +2619,7 @@ Notation "''Z' ( R )" := (center_mx R) : matrix_set_scope. 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_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}. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 699a1ba..b90b35a 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1839,8 +1839,8 @@ 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 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}. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 53a933a..6d18825 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1662,8 +1662,8 @@ Arguments big_enum_val [R idx op I A] F. Arguments big_enum_rank [R idx op I A x] xA F. Arguments pair_big_dep [R idx op I J]. Arguments pair_big [R idx op I J]. -Arguments big_allpairs_dep [R idx op I1 I2 J h r1 r2 F]. -Arguments big_allpairs [R idx op I1 I2 r1 r2 F]. +Arguments big_allpairs_dep {R idx op I1 I2 J h r1 r2 F}. +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]. |