diff --git a/CHANGELOG.md b/CHANGELOG.md
index 92bfbe9eb9a602dbe39d8b20f1a65fb67df5f07e..d573da1160c8ca91f8df3deb16a41f2279adc0e0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -50,6 +50,8 @@ Coq 8.13 is no longer supported.
 - Make `persistently_True` a bi-entailment; this changes the default `rewrite`
   direction.
 - Make `BiLaterContractive` a class instead of a notation.
+- Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
+  classes `Typeclasses Opaque`.
 
 **Changes in `proofmode`:**
 
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.
diff --git a/tests/bi.ref b/tests/bi.ref
index 3501bc76ecfd2a8f1b503ae9b870dda364b97a14..27b5cb7da314682827854e7c3ab45e03ea45a9bb 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -4,3 +4,19 @@ PROP : bi
 m : gmap nat nat
 The term "m" has type "gmap nat nat" while it is expected to have type
  "gmap nat Z" (cannot unify "nat" and "Z").
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+In environment:
+PROP : bi
+P : PROP
+
+?p : "Persistent (|==> P)"
+
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+In environment:
+PROP : bi
+P : PROP
+
+?p : "Persistent (â–  P)"
+
diff --git a/tests/bi.v b/tests/bi.v
index 299a8bd3da335b979195624b4babcb3919896555..3e38ccce0141b0fe4696c2d13840e7c2170ea205 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -60,3 +60,13 @@ Section big_sepM_implicit_type.
   Definition big_sepM_implicit_type {PROP : bi} (m : gmap nat nat) : PROP :=
     [∗ map] x ∈ m, ⌜ 10%Z = x ⌝.
 End big_sepM_implicit_type.
+
+(** This tests that [bupd] is [Typeclasses Opaque]. If [bupd] were transparent,
+Coq would unify [bupd_instance] with [persistently]. *)
+Goal ∀ {PROP : bi} (P : PROP),
+  ∃ bupd_instance, Persistent (@bupd PROP bupd_instance P).
+Proof. intros. eexists _. Fail apply _. Abort.
+(* Similarly for [plainly]. *)
+Goal ∀ {PROP : bi} (P : PROP),
+  ∃ plainly_instance, Persistent (@plainly PROP plainly_instance P).
+Proof. intros. eexists _. Fail apply _. Abort.