make bi relations work again, and changelog

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`:**
 

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.