From faa2b32bac7454bcec366d9790b6f14331e297b0 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 6 Jan 2020 12:02:47 +0100
Subject: Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)

---
 mathcomp/algebra/mxalgebra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra/mxalgebra.v')

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}.
-- 
cgit v1.2.3