diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index db8e78d06bda139f1a58b14e60fbba059909f683..969801c7010640936f81f57e97b4b6686d5aa538 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -49,7 +49,7 @@ Global Instance lookup_ne k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
-Global Instance alter_ne f k n :
+Global Instance alter_ne (f : A → A) (k : K) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
 Proof.
   intros ? m m' Hm k'.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index c39d29610e8f78ae37aa651540c239461a2974fa..e8a433af888b5d15fdf792b0d14ca5499fdd068c 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -340,13 +340,13 @@ Section properties.
     rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
   Qed.
 
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
     by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
   Qed.
   Lemma list_op_singletonM i (x y : A) :
-    {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
+    {[ i := x ]} ⋅ {[ i := y ]} ≡@{list A} {[ i := x ⋅ y ]}.
   Proof.
     rewrite /singletonM /list_singletonM /=.
     induction i; constructor; rewrite ?left_id; auto.