From 5b31a9e767694ce134fdff4461a876411eba0f2d Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Thu, 10 Sep 2020 18:15:25 +0200
Subject: rename mem_imset2 to imset2_f (with deprecation)

---
 mathcomp/character/vcharacter.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/character')

diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index faecc02..e1c7ec4 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -696,7 +696,7 @@ have [j def_chi_j]: {j | 'chi_j = phi}.
 exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx].
 rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //.
 rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy.
-by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV.
+by rewrite -(conjgK y x) cover_imset -class_supportEr imset2_f ?groupV.
 Qed.
 
 End MoreVchar.
-- 
cgit v1.2.3