From cf77729634c9b6ad1759d7b8e19e4fa8a5ee433c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 May 2023 10:21:04 +0200
Subject: [PATCH] make bi relations work again, and changelog

---
 CHANGELOG.md            | 2 ++
 iris/bi/lib/relations.v | 7 ++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d573da116..076e6a025 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 ad42b9b9f..a60458654 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.
-- 
GitLab