diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index bcb3753478470501ff99a50d3c0e3005d2fff146..ab9189f10029f3eda012b52257a0e6590a7fba1e 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -272,14 +272,14 @@ End ucmra_mixin.
 #[projections(primitive=no)] (* FIXME: making this primitive means we cannot use
 the projections with eauto any more (see https://github.com/coq/coq/issues/17561) *)
 Class CmraDiscrete (A : cmra) := {
-  cmra_discrete_ofe_discrete :> OfeDiscrete A;
+  #[global] cmra_discrete_ofe_discrete :: OfeDiscrete A;
   cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
 }.
 Global Hint Mode CmraDiscrete ! : typeclass_instances.
 
 (** * Morphisms *)
 Class CmraMorphism {A B : cmra} (f : A → B) := {
-  cmra_morphism_ne :> NonExpansive f;
+  #[global] cmra_morphism_ne :: NonExpansive f;
   cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
   cmra_morphism_pcore x : f <$> pcore x ≡ pcore (f x);
   cmra_morphism_op x y : f (x ⋅ y) ≡ f x ⋅ f y
@@ -848,7 +848,7 @@ Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
 Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  #[global] rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Global Hint Mode rFunctorContractive ! : typeclass_instances.
 
@@ -942,7 +942,7 @@ Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
 Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  #[global] urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Global Hint Mode urFunctorContractive ! : typeclass_instances.
 
diff --git a/iris/algebra/monoid.v b/iris/algebra/monoid.v
index eb92af8fefa5ad34a56b718d3ff2c04095b47d3c..0fb9ea500f0828919c99f5a4028808bdab5a654d 100644
--- a/iris/algebra/monoid.v
+++ b/iris/algebra/monoid.v
@@ -46,7 +46,7 @@ Class WeakMonoidHomomorphism {M1 M2 : ofe}
 Class MonoidHomomorphism {M1 M2 : ofe}
     (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) `{!Monoid o1, !Monoid o2}
     (R : relation M2) (f : M1 → M2) := {
-  monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 R f;
+  #[global] monoid_homomorphism_weak :: WeakMonoidHomomorphism o1 o2 R f;
   monoid_homomorphism_unit : R (f monoid_unit) monoid_unit
 }.
 
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index b3b0c99f2cfe6db48b91529a162dcea9ff9b0260..a6555c3f887d4562e545fe2123a3b4fc8aa13aed 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -130,7 +130,7 @@ Global Arguments discrete_0 {_} _ {_} _ _.
 Global Hint Mode Discrete + ! : typeclass_instances.
 Global Instance: Params (@Discrete) 1 := {}.
 
-Class OfeDiscrete (A : ofe) := ofe_discrete_discrete (x : A) :> Discrete x.
+Class OfeDiscrete (A : ofe) := #[global] ofe_discrete_discrete (x : A) :: Discrete x.
 Global Hint Mode OfeDiscrete ! : typeclass_instances.
 
 (** OFEs with a completion *)
@@ -939,7 +939,7 @@ Delimit Scope oFunctor_scope with OF.
 Bind Scope oFunctor_scope with oFunctor.
 
 Class oFunctorContractive (F : oFunctor) :=
-  oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  #[global] oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} ::
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Global Hint Mode oFunctorContractive ! : typeclass_instances.
 
diff --git a/iris/algebra/proofmode_classes.v b/iris/algebra/proofmode_classes.v
index ea29088847fff5cf7610c2670b50b39a3f97293c..05ca50a3c146ce938807f6d4ab83b8f99c863807 100644
--- a/iris/algebra/proofmode_classes.v
+++ b/iris/algebra/proofmode_classes.v
@@ -35,7 +35,7 @@ Global Hint Mode IsOp + - - - : typeclass_instances.
 Global Instance is_op_op {A : cmra} (a b : A) : IsOp (a â‹… b) a b | 100.
 Proof. by rewrite /IsOp. Qed.
 
-Class IsOp' {A : cmra} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
+Class IsOp' {A : cmra} (a b1 b2 : A) := #[global] is_op' :: IsOp a b1 b2.
 Global Hint Mode IsOp' + ! - - : typeclass_instances.
 Global Hint Mode IsOp' + - ! ! : typeclass_instances.
 
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index d35b2c3a6a556f58938f9eab55cdf05dd2e81e5f..95d08b51ec7e9ac00a2281266d2ef2f79aeb50c3 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -49,7 +49,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
 }.
 
 Class BiEmbed (PROP1 PROP2 : bi) := {
-  bi_embed_embed :> Embed PROP1 PROP2;
+  #[global] bi_embed_embed :: Embed PROP1 PROP2;
   bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
 }.
 Global Hint Mode BiEmbed ! - : typeclass_instances.
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
index f665cae03ed29b201a44e4103d49b251c2ef42fd..eec90d5ff94a63d1c040f5ca7a4bdd56cb3300b1 100644
--- a/iris/bi/extensions.v
+++ b/iris/bi/extensions.v
@@ -26,7 +26,7 @@ Global Hint Mode BiLöb ! : typeclass_instances.
 Global Arguments löb_weak {_ _} _ _.
 
 Class BiLaterContractive (PROP : bi) :=
-  later_contractive :> Contractive (bi_later (PROP:=PROP)).
+  #[global] later_contractive :: Contractive (bi_later (PROP:=PROP)).
 
 (** The class [BiPersistentlyForall] states that universal quantification
 commutes with the persistently modality. The reverse direction of the entailment
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index b2dc63131ca2822266b8c255cdef335cb0fc0754..7817ce480deba954bcebbf422727703ce6401f14 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -45,7 +45,7 @@ Record BiInternalEqMixin (PROP : bi) `(!InternalEq PROP) := {
 }.
 
 Class BiInternalEq (PROP : bi) := {
-  bi_internal_eq_internal_eq :> InternalEq PROP;
+  #[global] bi_internal_eq_internal_eq :: InternalEq PROP;
   bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
 }.
 Global Hint Mode BiInternalEq ! : typeclass_instances.
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index f3a8b9a20f46e2d9f19823c2242b48da1a74daed..65fca318a02bc042656e7618ea54ab226a2102dd 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -149,4 +149,4 @@ Section internal_included_laws.
     + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
     + iIntros "H". by iExists _.
   Qed.
-End internal_included_laws.
\ No newline at end of file
+End internal_included_laws.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index af0e93e30e70733e9b149091f3b17ddb7de18409..39a85f852b8de34f1ca7b0779df181f89914d21e 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -44,7 +44,7 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
 }.
 
 Class BiPlainly (PROP : bi) := {
-  bi_plainly_plainly :> Plainly PROP;
+  #[global] bi_plainly_plainly :: Plainly PROP;
   bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
 }.
 Global Hint Mode BiPlainly ! : typeclass_instances.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 964b4567a7d8b3e865252e171927da89aa1a6504..bded5423ae90762c341636585f6df2c8fd5908bb 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -92,14 +92,14 @@ Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
 }.
 
 Class BiBUpd (PROP : bi) := {
-  bi_bupd_bupd :> BUpd PROP;
+  #[global] bi_bupd_bupd :: BUpd PROP;
   bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
 }.
 Global Hint Mode BiBUpd ! : typeclass_instances.
 Global Arguments bi_bupd_bupd : simpl never.
 
 Class BiFUpd (PROP : bi) := {
-  bi_fupd_fupd :> FUpd PROP;
+  #[global] bi_fupd_fupd :: FUpd PROP;
   bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
 }.
 Global Hint Mode BiFUpd ! : typeclass_instances.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 820148a1386840f4b69e84aac35dbc33ace645f5..11c858928af623c7ad6d333bf9d888a914307e25 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -35,7 +35,7 @@ Definition ownPΣ (Λ : language) : gFunctors :=
     GFunctor (excl_authR (stateO Λ))].
 
 Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
-  ownPPre_invG :> invGpreS Σ;
+  #[global] ownPPre_invG :: invGpreS Σ;
   ownPPre_state_inG : inG Σ (excl_authR (stateO Λ))
 }.
 Local Existing Instance ownPPre_state_inG.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 11741d78ce21af703f5b89a6b9aa8309dc6b7332..a91163e7ae3a6bd933d5ac10d8678c7862a72d22 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class irisGS_gen (hlc : has_lc) (Λ : language) (Σ : gFunctors) := IrisG {
-  iris_invGS :> invGS_gen hlc Σ;
+  #[global] iris_invGS :: invGS_gen hlc Σ;
 
   (** The state interpretation is an invariant that should hold in
   between each step of reduction. Here [Λstate] is the global state,
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index dac8d87d9660435992fa98cce9db2163997053cb..d9e4f7a882767a6372d49ea8b812017b9851a77f 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -17,13 +17,13 @@ Global Arguments from_assumption {_} _ _%I _%I {_}.
 Global Hint Mode FromAssumption + + - - : typeclass_instances.
 
 Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
-  knownl_from_assumption :> FromAssumption p P Q.
+  #[global] knownl_from_assumption :: FromAssumption p P Q.
 Global Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
 Global Arguments knownl_from_assumption {_} _ _%I _%I {_}.
 Global Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
 
 Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
-  knownr_from_assumption :> FromAssumption p P Q.
+  #[global] knownr_from_assumption :: FromAssumption p P Q.
 Global Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
 Global Arguments knownr_from_assumption {_} _ _%I _%I {_}.
 Global Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
@@ -444,7 +444,7 @@ Global Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
 Global Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
 
 Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
-  into_laterN :> MaybeIntoLaterN only_head n P Q.
+  #[global] into_laterN :: MaybeIntoLaterN only_head n P Q.
 Global Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
 Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
 
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index 4af72163fd943e245b8abd70d85bfb8b093b4eae..c173bfd2f5bbd1ae75381020f390e64f76ebf5d5 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -55,7 +55,7 @@ Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :
 Global Arguments MakeEmbed {_ _ _} _%I _%I.
 Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
 Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
-  known_make_embed :> MakeEmbed P Q.
+  #[global] known_make_embed :: MakeEmbed P Q.
 Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
 Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
 
@@ -63,11 +63,11 @@ Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
 Global Arguments MakeSep {_} _%I _%I _%I.
 Global Hint Mode MakeSep + - - - : typeclass_instances.
 Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_sep :> MakeSep P Q PQ.
+  #[global] knownl_make_sep :: MakeSep P Q PQ.
 Global Arguments KnownLMakeSep {_} _%I _%I _%I.
 Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
 Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
-  knownr_make_sep :> MakeSep P Q PQ.
+  #[global] knownr_make_sep :: MakeSep P Q PQ.
 Global Arguments KnownRMakeSep {_} _%I _%I _%I.
 Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
 
@@ -75,11 +75,11 @@ Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
 Global Arguments MakeAnd {_} _%I _%I _%I.
 Global Hint Mode MakeAnd + - - - : typeclass_instances.
 Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_and :> MakeAnd P Q PQ.
+  #[global] knownl_make_and :: MakeAnd P Q PQ.
 Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
 Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
 Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
-  knownr_make_and :> MakeAnd P Q PQ.
+  #[global] knownr_make_and :: MakeAnd P Q PQ.
 Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
 Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
 
@@ -87,10 +87,10 @@ Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
 Global Arguments MakeOr {_} _%I _%I _%I.
 Global Hint Mode MakeOr + - - - : typeclass_instances.
 Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
-  knownl_make_or :> MakeOr P Q PQ.
+  #[global] knownl_make_or :: MakeOr P Q PQ.
 Global Arguments KnownLMakeOr {_} _%I _%I _%I.
 Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
-Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
+Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := #[global] knownr_make_or :: MakeOr P Q PQ.
 Global Arguments KnownRMakeOr {_} _%I _%I _%I.
 Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
 
@@ -99,7 +99,7 @@ Class MakeAffinely {PROP : bi} (P Q : PROP) :=
 Global Arguments MakeAffinely {_} _%I _%I.
 Global Hint Mode MakeAffinely + - - : typeclass_instances.
 Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
-  known_make_affinely :> MakeAffinely P Q.
+  #[global] known_make_affinely :: MakeAffinely P Q.
 Global Arguments KnownMakeAffinely {_} _%I _%I.
 Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
 
@@ -108,7 +108,7 @@ Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
 Global Arguments MakeIntuitionistically {_} _%I _%I.
 Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
 Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
-  known_make_intuitionistically :> MakeIntuitionistically P Q.
+  #[global] known_make_intuitionistically :: MakeIntuitionistically P Q.
 Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
 Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
 
@@ -117,7 +117,7 @@ Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
 Global Arguments MakeAbsorbingly {_} _%I _%I.
 Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
 Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
-  known_make_absorbingly :> MakeAbsorbingly P Q.
+  #[global] known_make_absorbingly :: MakeAbsorbingly P Q.
 Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
 Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
 
@@ -126,7 +126,7 @@ Class MakePersistently {PROP : bi} (P Q : PROP) :=
 Global Arguments MakePersistently {_} _%I _%I.
 Global Hint Mode MakePersistently + - - : typeclass_instances.
 Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
-  known_make_persistently :> MakePersistently P Q.
+  #[global] known_make_persistently :: MakePersistently P Q.
 Global Arguments KnownMakePersistently {_} _%I _%I.
 Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
 
@@ -135,7 +135,7 @@ Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
 Global Arguments MakeLaterN {_} _%nat _%I _%I.
 Global Hint Mode MakeLaterN + + - - : typeclass_instances.
 Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
-  known_make_laterN :> MakeLaterN n P lP.
+  #[global] known_make_laterN :: MakeLaterN n P lP.
 Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
 Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
 
@@ -144,6 +144,6 @@ Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
 Global Arguments MakeExcept0 {_} _%I _%I.
 Global Hint Mode MakeExcept0 + - - : typeclass_instances.
 Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
-  known_make_except_0 :> MakeExcept0 P Q.
+  #[global] known_make_except_0 :: MakeExcept0 P Q.
 Global Arguments KnownMakeExcept0 {_} _%I _%I.
 Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
diff --git a/iris_deprecated/base_logic/auth.v b/iris_deprecated/base_logic/auth.v
index 303e36405fe71cf63edd7ab28b46afcbd67dc843..17de712d3e09a4970669c41fe8bbde8e8e604349 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -12,7 +12,7 @@ Import uPred.
 (* The CMRA we need. *)
 Class authG Σ (A : ucmra) := AuthG {
   auth_inG : inG Σ (authR A);
-  auth_cmra_discrete :> CmraDiscrete A;
+  #[global] auth_cmra_discrete :: CmraDiscrete A;
 }.
 Local Existing Instance auth_inG.
 
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index b20282c006769efed15dd7f9ae5380f5bfec1825..e6317ab4db802afd2bceb5f3c5cfd5515fd52bee 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -11,7 +11,7 @@ Import uPred.
 (** The CMRA we need. *)
 Class stsG Σ (sts : stsT) := StsG {
   sts_inG : inG Σ (sts_resR sts);
-  sts_inhabited :> Inhabited (sts.state sts);
+  #[global] sts_inhabited :: Inhabited (sts.state sts);
 }.
 Local Existing Instance sts_inG.
 
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index 34ace6793daa9c77172f64434835eeab20441ee6..3691d5127f1305d83ac6a40e74b900752bcf8726 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -6,11 +6,11 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 Class heapGpreS Σ := HeapGpreS {
-  heapGpreS_iris :> invGpreS Σ;
-  heapGpreS_heap :> gen_heapGpreS loc (option val) Σ;
-  heapGpreS_inv_heap :> inv_heapGpreS loc (option val) Σ;
-  heapGpreS_proph :> proph_mapGpreS proph_id (val * val) Σ;
-  heapGS_step_cnt :> mono_natG Σ;
+  #[global] heapGpreS_iris :: invGpreS Σ;
+  #[global] heapGpreS_heap :: gen_heapGpreS loc (option val) Σ;
+  #[global] heapGpreS_inv_heap :: inv_heapGpreS loc (option val) Σ;
+  #[global] heapGpreS_proph :: proph_mapGpreS proph_id (val * val) Σ;
+  #[global] heapGS_step_cnt :: mono_natG Σ;
 }.
 
 Definition heapΣ : gFunctors :=
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 7b02c63598df7020f8b6698fefb3835208a4e828..055e10fc6d30bfd83f03b1d52581438742b2980d 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -38,13 +38,13 @@ Class atomic_heap := AtomicHeap {
   (* -- predicates -- *)
   pointsto `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (dq: dfrac) (v : val) : iProp Σ;
   (* -- pointsto properties -- *)
-  pointsto_timeless `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :>
+  #[global] pointsto_timeless `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v ::
     Timeless (pointsto (H:=H) l q v);
-  pointsto_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :>
+  #[global] pointsto_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v ::
     Fractional (λ (q : Qp), pointsto (H:=H) l (DfracOwn q) v);
-  pointsto_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :>
+  #[global] pointsto_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v ::
     Persistent (pointsto (H:=H) l DfracDiscarded v);
-  pointsto_as_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :>
+  #[global] pointsto_as_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v ::
     AsFractional (pointsto (H:=H) l (DfracOwn q) v) (λ q, pointsto (H:=H) l (DfracOwn q) v) q;
   pointsto_agree `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq1 dq2 v1 v2 :
     pointsto (H:=H) l dq1 v1 -∗ pointsto (H:=H) l dq2 v2 -∗ ⌜v1 = v2⌝;
diff --git a/iris_heap_lang/lib/lock.v b/iris_heap_lang/lib/lock.v
index b06b4f1cbe3f40bad6e92b8a84aac74f30061949..d7010e93c6c29c36438ff7a831a279b82269aa86 100644
--- a/iris_heap_lang/lib/lock.v
+++ b/iris_heap_lang/lib/lock.v
@@ -32,11 +32,11 @@ Class lock := Lock {
   is_lock `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_lock_persistent `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :>
+  #[global] is_lock_persistent `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R ::
     Persistent (is_lock (L:=L) γ lk R);
   is_lock_iff `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R1 R2 :
     is_lock (L:=L) γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock (L:=L) γ lk R2;
-  locked_timeless `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :>
+  #[global] locked_timeless `{!heapGS_gen hlc Σ} {L : lockG Σ} γ ::
     Timeless (locked (L:=L) γ);
   locked_exclusive `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :
     locked (L:=L) γ -∗ locked (L:=L) γ -∗ False;
diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 57060fd9814e4bde566e6519d7c2c0a4c3c0c8ec..b7bbeee50068f07ca6d0905dc68629e10f488ff1 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -37,13 +37,13 @@ Class rwlock := RwLock {
   reader_locked `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (γ : lock_name) (q : Qp) : iProp Σ;
   writer_locked `{!heapGS_gen hlc Σ} {L : rwlockG Σ} (γ : lock_name) : iProp Σ;
   (** * General properties of the predicates *)
-  is_rw_lock_persistent `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ :>
+  #[global] is_rw_lock_persistent `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ ::
     Persistent (is_rw_lock (L:=L) γ lk Φ);
   is_rw_lock_iff `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ lk Φ Ψ :
     is_rw_lock (L:=L) γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock (L:=L) γ lk Ψ;
-  reader_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ q :>
+  #[global] reader_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ q ::
     Timeless (reader_locked (L:=L) γ q);
-  writer_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ :>
+  #[global] writer_locked_timeless `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ ::
     Timeless (writer_locked (L:=L) γ);
   writer_locked_exclusive `{!heapGS_gen hlc Σ} {L : rwlockG Σ} γ :
     writer_locked (L:=L) γ -∗ writer_locked (L:=L) γ -∗ False;
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 43bd589d15c38174addc3bfd6005aee348417196..aaf3079579ee7ffbe2ccdc778cae7420be1e8f2e 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -13,9 +13,9 @@ From iris.prelude Require Import options.
 
 Class heapGS_gen hlc Σ := HeapGS {
   heapGS_invGS : invGS_gen hlc Σ;
-  heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
-  heapGS_inv_heapGS :> inv_heapGS loc (option val) Σ;
-  heapGS_proph_mapGS :> proph_mapGS proph_id (val * val) Σ;
+  #[global] heapGS_gen_heapGS :: gen_heapGS loc (option val) Σ;
+  #[global] heapGS_inv_heapGS :: inv_heapGS loc (option val) Σ;
+  #[global] heapGS_proph_mapGS :: proph_mapGS proph_id (val * val) Σ;
   heapGS_step_name : gname;
   heapGS_step_cnt : mono_natG Σ;
 }.
diff --git a/tests/iprop.v b/tests/iprop.v
index 7cbb7359d883150e211918b5ebd78aed2e85eaeb..edfb9106277a056e910ac720b957be54b2ae3619 100644
--- a/tests/iprop.v
+++ b/tests/iprop.v
@@ -21,4 +21,4 @@ From iris.base_logic Require Import iprop.
 Lemma bi_ofeO_iProp Σ : bi_ofeO (iPropI Σ) = iPropO Σ.
 Proof. reflexivity. Qed.
 Lemma bi_cofe_iProp Σ : bi_cofe (iPropI Σ) = @uPred_cofe (iResUR Σ).
-Proof. reflexivity. Qed.
\ No newline at end of file
+Proof. reflexivity. Qed.