From 7665002c0b01dbb0200a21476829b127993ce8ba Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 21 Mar 2025 14:01:33 +0100
Subject: [PATCH] adapt to rocq#19987

---
 theories/PFsection2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/PFsection2.v b/theories/PFsection2.v
index d1ed67d..0e642f4 100644
--- a/theories/PFsection2.v
+++ b/theories/PFsection2.v
@@ -582,7 +582,7 @@ rewrite big1 ?add0r => [|x /andP[calAx not_nBaLx]]; last first.
   by apply/pred0Pn; exists g; apply/andP.
 rewrite (partition_big fBg (mem nBaL)) /= => [|x]; last by case/andP.
 apply: eq_bigr => b; case/setIP=> Nb aLb; rewrite mulr_natr -sumr_const.
-apply: eq_big => x; rewrite ![x \in _]inE -!andbA.
+apply: eq_big => x; rewrite ![_ \in calA _ _]inE -!andbA.
   apply: andb_id2l=> Gx; apply/and3P/idP=> [[Mgx _] /eqP <- | HBb_gx].
     by rewrite mem_rcoset mem_divgr ?mulHNB.
   suffices ->: fBg x = b.