diff --git a/CHANGELOG.md b/CHANGELOG.md
index d573da1160c8ca91f8df3deb16a41f2279adc0e0..076e6a025b459cf12b9f0d3559ec90e18898e88c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -52,6 +52,8 @@ Coq 8.13 is no longer supported.
 - Make `BiLaterContractive` a class instead of a notation.
 - Make projections of `Bupd`/`Fupd`/`InternalEq`/`Plainly` operational type
   classes `Typeclasses Opaque`.
+- Make BI relations (`bi_rtc`, `bi_tc`, `bi_nsteps`) typeclasses opaque (they
+  were accidentally transparent).
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index ad42b9b9fcb9b32f1163a909d37633da9532d11d..a60458654dc9dcb2eb60053851578470d6bef900 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -21,7 +21,6 @@ Section definitions.
     bi_least_fixpoint (bi_rtc_pre R x2) x1.
 
   Global Instance: Params (@bi_rtc) 4 := {}.
-  Global Typeclasses Opaque bi_rtc.
 
   Local Definition bi_tc_pre (R : A → A → PROP)
       (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
@@ -32,7 +31,6 @@ Section definitions.
     bi_least_fixpoint (bi_tc_pre R x2) x1.
 
   Global Instance: Params (@bi_tc) 4 := {}.
-  Global Typeclasses Opaque bi_tc.
 
   (** Reductions of exactly [n] steps. *)
   Fixpoint bi_nsteps (R : A → A → PROP) (n : nat) (x1 x2 : A) : PROP :=
@@ -42,7 +40,6 @@ Section definitions.
     end.
 
   Global Instance: Params (@bi_nsteps) 5 := {}.
-  Global Typeclasses Opaque bi_nsteps.
 End definitions.
 
 Local Instance bi_rtc_pre_mono {PROP : bi} `{!BiInternalEq PROP}
@@ -418,3 +415,7 @@ Section timeless.
     ∀ x y, Timeless (bi_tc R x y).
   Proof. intros ? x y. rewrite bi_tc_nsteps. apply _. Qed.
 End timeless.
+
+Global Typeclasses Opaque bi_rtc.
+Global Typeclasses Opaque bi_tc.
+Global Typeclasses Opaque bi_nsteps.