Make some definitions local

iris/bi/lib/relations.v

@@ -12,7 +12,7 @@ Section definitions.
   Context {PROP : bi} `{!BiInternalEq PROP}.
   Context {A : ofe}.
 
-  Definition bi_rtc_pre (R : A → A → PROP)
+  Local Definition bi_rtc_pre (R : A → A → PROP)
       (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
     <affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
 
@@ -23,7 +23,7 @@ Section definitions.
   Global Instance: Params (@bi_rtc) 4 := {}.
   Typeclasses Opaque bi_rtc.
 
-  Definition bi_tc_pre (R : A → A → PROP)
+  Local Definition bi_tc_pre (R : A → A → PROP)
       (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
     R x1 x2 ∨ ∃ x', R x1 x' ∗ rec x'.