From e565f8d9bebd4fd681c34086d5448dbaebc11976 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 19 Nov 2020 18:33:21 +0100
Subject: Removing duplicate clears and turning the warning into an error

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

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

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 77d2e4f..9b27ba7 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1650,7 +1650,7 @@ Lemma diagmx_ind (P : forall m n, 'M_(m, n) -> Type) :
   forall m n A, is_diag_mx A -> P m n A.
 Proof.
 move=> P0l P0r PS m n A Adiag; have Atrig := is_diag_mx_is_trig Adiag.
-elim/trigmx_ind: Atrig Adiag => // {m n} m n r c {A}A _ PA.
+elim/trigmx_ind: Atrig Adiag => // {}m {}n r c {}A _ PA.
 rewrite is_diag_block_mx => // /and4P[_ /eqP-> _ Adiag].
 exact: PS (PA _).
 Qed.
@@ -1660,7 +1660,7 @@ Lemma diagsqmx_ind (P : forall n, 'M[V]_n -> Type) :
   (forall n x c A, is_diag_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) ->
   forall n A, is_diag_mx A -> P n A.
 Proof.
-move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA.
+move=> P0 PS n A; elim/sqmx_ind: A => [|{}n x r c] A PA.
   by rewrite thinmx0; apply: P0.
 rewrite is_diag_block_mx => // /and4P[/eqP-> /eqP-> _ Adiag].
 exact: PS (PA _).
-- 
cgit v1.2.3