From bba50f731e6d420f1c3a47efa7c41973046cfd23 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 5 Feb 2024 16:59:00 +0100
Subject: [PATCH] Get rid of future-coercion-class-field warnings

---
 iris/algebra/cmra.v               |  8 ++++----
 iris/algebra/monoid.v             |  2 +-
 iris/algebra/ofe.v                |  4 ++--
 iris/algebra/proofmode_classes.v  |  2 +-
 iris/bi/embedding.v               |  2 +-
 iris/bi/extensions.v              |  2 +-
 iris/bi/internal_eq.v             |  2 +-
 iris/bi/lib/cmra.v                |  2 +-
 iris/bi/plainly.v                 |  2 +-
 iris/bi/updates.v                 |  4 ++--
 iris/program_logic/ownp.v         |  2 +-
 iris/program_logic/weakestpre.v   |  2 +-
 iris/proofmode/classes.v          |  6 +++---
 iris/proofmode/classes_make.v     | 26 +++++++++++++-------------
 iris_deprecated/base_logic/auth.v |  2 +-
 iris_deprecated/base_logic/sts.v  |  2 +-
 iris_heap_lang/adequacy.v         | 10 +++++-----
 iris_heap_lang/lib/atomic_heap.v  |  8 ++++----
 iris_heap_lang/lib/lock.v         |  4 ++--
 iris_heap_lang/lib/rw_lock.v      |  6 +++---
 iris_heap_lang/primitive_laws.v   |  6 +++---
 tests/iprop.v                     |  2 +-
 22 files changed, 53 insertions(+), 53 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index bcb375347..ab9189f10 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 eb92af8fe..0fb9ea500 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 b3b0c99f2..a6555c3f8 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 ea2908884..05ca50a3c 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 d35b2c3a6..95d08b51e 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 f665cae03..eec90d5ff 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 b2dc63131..7817ce480 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 f3a8b9a20..65fca318a 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 af0e93e30..39a85f852 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 964b4567a..bded5423a 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 820148a13..11c858928 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 11741d78c..a91163e7a 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 dac8d87d9..d9e4f7a88 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 4af72163f..c173bfd2f 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 303e36405..17de712d3 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 b20282c00..e6317ab4d 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 34ace6793..3691d5127 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 7b02c6359..055e10fc6 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 b06b4f1cb..d7010e93c 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 57060fd98..b7bbeee50 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 43bd589d1..aaf307957 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 7cbb7359d..edfb91062 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.
-- 
GitLab