diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 992400cac2f4e44a79c8b626d6ed7bf786df4e37..87b5a7cc741f95400ad5e89ee56c68ef185bf530 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
 
 Global Instance auth_frag_sep_homomorphism :
-  MonoidHomomorphism op op (≡) (Auth None).
+  MonoidHomomorphism op op (≡) (@Auth A None).
 Proof. by split; [split; try apply _|]. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index a4c6a03a727cd2165fb553fb6b0e148c1ad8de33..a0fd519b00d28b13f1a2587cd4b7c4acd91a7cdd 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -25,7 +25,7 @@ Section ofe.
     by destruct (decide _) as [[]|].
   Qed.
   Global Instance ofe_fun_insert_proper x :
-    Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert x) := ne_proper_2 _.
+    Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert (B:=B) x) := ne_proper_2 _.
 
   Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
   Proof.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a09b287e85b6afdfd71b15e2226985ae528e6e50..b9a995537ea553ed15d6c179b48769353d47beb4 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
 Section cofe.
 Context `{Countable K} {A : ofeT}.
 Implicit Types m : gmap K A.
+Implicit Types i : K.
 
 Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ≡{n}≡ m2 !! i.