diff --git a/CHANGELOG.md b/CHANGELOG.md
index f77e7b16f6171d5053bf7868555c62ff8cdf083b..12133236b2f86e6adf82c06756345fde91ef1554 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,11 @@
 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
+## std++ master
+
+- Generalize `foldr_comm_acc`, `map_fold_comm_acc`, `set_fold_comm_acc`, and
+  `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
+
 ## std++ 1.10.0 (2024-04-12)
 
 The highlight of this release is the bitvector library with support for
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 85eecad3503d32746806fb1aad0dd65ea7882d5e..87f1f2c5b5f4654fcf7bfc75b126c15a6f1ba847 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1443,7 +1443,7 @@ Proof.
     apply Hgm'. rewrite lookup_insert_ne by naive_solver. done.
 Qed.
 
-Lemma map_fold_comm_acc {A} (f : K → A → A → A) (g : A → A) (x : A) (m : M A) :
+Lemma map_fold_comm_acc {A B} (f : K → A → B → B) (g : B → B) (x : B) (m : M A) :
   (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
   (∀ j z y, f j z (g y) = g (f j z y)) →
   map_fold f (g x) m = g (map_fold f x m).
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index 01e3bf7a723e287e808fee0e34785e8947ecbdc2..85b7b42e1b9b9605df5c9db19219ff7a85bcb456 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -339,9 +339,9 @@ Proof.
   intros. unfold set_fold; simpl.
   apply foldr_comm_acc_strong; [done|solve_proper|set_solver].
 Qed.
-Lemma set_fold_comm_acc (f : A → A → A) (g : A → A) (a : A) X :
+Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
   (∀ x y, f x (g y) = g (f x y)) →
-  set_fold f (g a) X = g (set_fold f a X).
+  set_fold f (g b) X = g (set_fold f b X).
 Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
 
 (** * Minimal elements *)
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index d92d40858557b1da57bc243df4e5b850192ed5ca..d7fcff4068828741df23860f1aedd40231ab6042 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -599,9 +599,9 @@ Section more_lemmas.
     apply foldr_comm_acc_strong; [done|solve_proper|].
     intros. by apply Hfg, gmultiset_elem_of_elements.
   Qed.
-  Lemma gmultiset_set_fold_comm_acc (f : A → A → A) (g : A → A) (a : A) X :
+  Lemma gmultiset_set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
     (∀ x c, g (f x c) = f x (g c)) →
-    set_fold f (g a) X = g (set_fold f a X).
+    set_fold f (g b) X = g (set_fold f b X).
   Proof.
     intros. apply (gmultiset_set_fold_comm_acc_strong _); [solve_proper|done].
   Qed.
diff --git a/stdpp/list.v b/stdpp/list.v
index a146fcce440f21e8e2699629440dd03fc693be36..b3a076c436d6b579b2599f22a1c64f1a072238e4 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4691,9 +4691,9 @@ Proof.
   rewrite <-Hcomm by eauto using elem_of_list_here.
   by rewrite IH by eauto using elem_of_list_further.
 Qed.
-Lemma foldr_comm_acc {A} (f : A → A → A) (g : A → A) (a : A) l :
+Lemma foldr_comm_acc {A B} (f : A → B → B) (g : B → B) (b : B) l :
   (∀ x y, f x (g y) = g (f x y)) →
-  foldr f (g a) l = g (foldr f a l).
+  foldr f (g b) l = g (foldr f b l).
 Proof. intros. apply (foldr_comm_acc_strong _); [solve_proper|done]. Qed.
 
 Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :