diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index dd1da98a50bdfde9d36562d055d2496fb26e6e27..4ea5f8f7bb50e5b822991dd3b7b8bf75830395dd 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -101,7 +101,8 @@ Section list.
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
-  Lemma big_opL_gen_proper_2 (R : relation M) f g l1 l2 :
+  Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
+        l1 (l2 : list B) :
     R monoid_unit monoid_unit →
     Proper (R ==> R ==> R) o →
     (∀ k,
@@ -230,8 +231,8 @@ Section gmap.
   Implicit Types m : gmap K A.
   Implicit Types f g : K → A → M.
 
-
-  Lemma big_opM_gen_proper_2 (R : relation M) f g m1 m2 :
+  Lemma big_opM_gen_proper_2 {B} (R : relation M) f (g : K → B → M)
+        m1 (m2 : gmap K B) :
     subrelation (≡) R → Equivalence R →
     Proper (R ==> R ==> R) o →
     (∀ k,