From 298830c5a3860c7a645df6effe7d1cc228d56150 Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Thu, 10 Sep 2020 17:45:57 +0200
Subject: rename mem_imset to imset_f (with deprecation)

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

(limited to 'mathcomp/character/classfun.v')

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 9c4557a..356ff5c 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2355,7 +2355,7 @@ Proof.
 have [[injg defR] [injh defS]] := (isomP isoG, isomP isoH).
 rewrite !morphimEdom in defS defR; apply/cfun_inP=> s.
 rewrite -{1}defS => /imsetP[x Hx ->] {s}; have Gx := subsetP sHG x Hx.
-rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?mem_imset // -defR.
+rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?imset_f // -defR.
 by rewrite (eq_in_imset eq_hg) imsetS.
 Qed.
 
-- 
cgit v1.2.3