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/solvable/maximal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/solvable/maximal.v')

diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 5af62c9..3786cff 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1544,7 +1544,7 @@ have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p.
 have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z.
   rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp).
     by rewrite (subsetP sX'A) //= mem_commg ?(subsetP sUX).
-  by rewrite groupMl -1?[x^-1]conjg1 mem_gen // mem_imset2 // ?groupV cycle_id.
+  by rewrite groupMl -1?[x^-1]conjg1 mem_gen // imset2_f // ?groupV cycle_id.
 have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY).
   by rewrite centsC in cZX; rewrite defXY (subsetP (centS sUX)) ?(subsetP cZX).
 rewrite -defU1 exponent_Ohm1_class2 // nil_class2 -defXY der1_joing_cycles //.
-- 
cgit v1.2.3