seq compatibility with math-comp/math-comp#790

Companion of math-comp#56, see math-comp#56 for explanation
JasonGross · Mar 3, 2023 · ac495a3 · ac495a3
1 parent b5e20bf
commit ac495a3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/freeg.v b/src/freeg.v
@@ -514,7 +514,7 @@ Section FreegTheory.
   Qed.
 
   Lemma Freeg_dom D:
-    [freeg [seq (coeff z D, z) | z <- dom D]] = D.
+    [freeg [seq (coeff x D, x) | x <- dom D]] = D.
   Proof.
     apply/esym/eqP/freeg_eqP=> k.
     rewrite -{1 2}[D]freeg_repr !coeff_Freeg /dom.
@@ -943,7 +943,7 @@ Section FreeglModType.
   Canonical freeg_lmodType :=
     Eval hnf in LmodType R {freeg K / R} freeg_lmodMixin.
 End FreeglModType.
-  
+
 (* -------------------------------------------------------------------- *)
 Section FreeglModTheory.
   Variable R : ringType.