From 1c03fed9bd5ab57b99405802f17d50ff0888f887 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 19 Nov 2020 20:37:16 +0100
Subject: Using Coq 8.10 ssreflect new features

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

(limited to 'mathcomp/character')

diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index e94e69f..4202c6e 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -5684,9 +5684,9 @@ elim: t => //=.
 - by move=> k _; apply/rowP=> i; rewrite !mxE /= nth_row_env nth_map_rVval.
 - by move=> x _; rewrite eval_mx_term.
 - by move=> x _; rewrite eval_mx_term.
-- move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite -{}IH1 // -{}IH2 //.
+- move=> t1 + t2 + /andP[rt1 rt2] => <-// <-//.
   by apply/rowP=> k; rewrite !mxE.
-- by move=> t1 IH1 rt1; rewrite -{}IH1 //; apply/rowP=> k; rewrite !mxE.
+- by move=> t1 + rt1 => <-//; apply/rowP=> k; rewrite !mxE.
 - move=> t1 IH1 n1 rt1; rewrite eval_mulmx eval_mx_term mul_scalar_mx.
   by rewrite scaler_nat {}IH1 //; elim: n1 => //= n1 IHn1; rewrite !mulrS IHn1.
 - by move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite eval_mulT IH1 ?IH2.
-- 
cgit v1.2.3