diff options
| author | SimonBoulier | 2020-01-06 12:02:47 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-01-08 12:01:31 +0100 |
| commit | faa2b32bac7454bcec366d9790b6f14331e297b0 (patch) | |
| tree | 3c2bf096950c722a496ce215bff3830aadf915a9 /mathcomp/algebra | |
| parent | c7fa2a1444d450bcebdeea47800fef1436690b6d (diff) | |
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 4 |
1 files changed, 2 insertions, 2 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}. |