diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 5f27454f6f71b8ed515711dd224d1dd5b98ff9ad..c7624ac1054e66029309163868588019b7fb043c 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -266,7 +266,7 @@ Module le_upd.
        with the basic updates. *)
     Local Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
     Proof.
-      split.
+      split; rewrite /bupd.
       - apply _.
       - apply le_upd_intro.
       - apply le_upd_mono.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index c5020d48eb8766b0e97dbb1f613feb2650fbeb38..1e7b3526a9322bc5fb2dde13df1ee852cc7f166f 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -16,6 +16,8 @@ Class InternalEq (PROP : Type) :=
 Global Arguments internal_eq {_ _ _} _ _ : simpl never.
 Global Hint Mode InternalEq ! : typeclass_instances.
 Global Instance: Params (@internal_eq) 3 := {}.
+Typeclasses Opaque internal_eq.
+
 Infix "≡" := internal_eq : bi_scope.
 Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
 
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 93d1e86b8e8bba08a83b05a316a6d441e53c183d..a8a50b3d6fc8eb17e21bbb69b22a6096987e54bb 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -15,6 +15,8 @@ Class Plainly (PROP : Type) := plainly : PROP → PROP.
 Global Arguments plainly {PROP}%type_scope {_} _%I.
 Global Hint Mode Plainly ! : typeclass_instances.
 Global Instance: Params (@plainly) 2 := {}.
+Typeclasses Opaque plainly.
+
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 359a8dc9eb29759bf65119e1b8c2a65c3e6e775c..8c6a60621e5d35bbdc2386be2bf70e2abd751f4c 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -17,6 +17,7 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Global Instance : Params (@bupd) 2 := {}.
 Global Hint Mode BUpd ! : typeclass_instances.
 Global Arguments bupd {_}%type_scope {_} _%bi_scope.
+Typeclasses Opaque bupd.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
 Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
@@ -26,6 +27,7 @@ Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Global Instance: Params (@fupd) 4 := {}.
 Global Hint Mode FUpd ! : typeclass_instances.
 Global Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
+Typeclasses Opaque fupd.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
 Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.