diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index c1a161dd2bd74a20150c12951ad4275d5a191c62..00a97edb94b40ff527ac82df7a5aa7b52c70742a 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -201,7 +201,7 @@ Section bupd_derived.
     - apply bupd_intro.
   Qed.
 
-  Global Instance bupd_homomorphism :
+  Global Instance bupd_sep_homomorphism :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (bupd (PROP:=PROP)).
   Proof. split; [split|]; try apply _; [apply bupd_sep | apply bupd_intro]. Qed.
 
@@ -381,7 +381,7 @@ Section fupd_derived.
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
 
-  Global Instance fupd_homomorphism E :
+  Global Instance fupd_sep_homomorphism E :
     MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (fupd (PROP:=PROP) E E).
   Proof. split; [split|]; try apply _; [apply fupd_sep | apply fupd_intro]. Qed.