From 5a3e60126ef771f446ec3ae79c0c257fb18996fa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 May 2023 21:52:16 +0200
Subject: [PATCH] Build without warnings.

---
 _CoqProject                                          |  2 --
 theories/barrier/example_joining_existentials.v      |  2 +-
 theories/barrier/proof.v                             |  4 ++--
 theories/concurrent_stacks/concurrent_stack2.v       |  2 +-
 theories/concurrent_stacks/concurrent_stack4.v       |  2 +-
 theories/hocap/cg_bag.v                              |  4 ++--
 theories/hocap/concurrent_runners.v                  |  2 +-
 theories/hocap/fg_bag.v                              |  2 +-
 theories/hocap/lib/oneshot.v                         |  2 +-
 theories/lecture_notes/ccounter.v                    |  2 +-
 theories/lecture_notes/coq_intro_example_2.v         |  6 +++---
 theories/lecture_notes/lock.v                        |  2 +-
 theories/lecture_notes/modular_incr.v                |  2 +-
 theories/lecture_notes/sfra.v                        |  4 ++--
 theories/locks/array_based_queuing_lock/abql.v       | 10 +++++-----
 theories/logatom/conditional_increment/cinc.v        |  6 +++---
 theories/logatom/counter_with_backup/counter_proof.v | 12 ++++++------
 theories/logatom/elimination_stack/hocap_spec.v      |  2 +-
 theories/logatom/elimination_stack/stack.v           |  4 ++--
 theories/logatom/flat_combiner/atomic_sync.v         |  2 +-
 theories/logatom/flat_combiner/flat.v                |  6 +++---
 theories/logatom/herlihy_wing_queue/hwq.v            |  8 ++++----
 theories/logatom/rdcss/rdcss.v                       |  6 +++---
 theories/logatom/snapshot/atomic_snapshot.v          |  4 ++--
 theories/logatom/treiber2.v                          |  2 +-
 theories/logrel/F_mu_ref_conc/binary/rules.v         |  2 +-
 theories/logrel/F_mu_ref_conc/unary/soundness.v      |  4 ++--
 theories/logrel/F_mu_ref_conc/wp_rules.v             |  2 +-
 theories/spanning_tree/mon.v                         |  6 +++---
 29 files changed, 56 insertions(+), 58 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 2d5f7bce..a5316e76 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,8 +4,6 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-# Fixing this one requires Coq 8.17
--arg -w -arg -future-coercion-class-field
 
 theories/barrier/proof.v
 theories/barrier/specification.v
diff --git a/theories/barrier/example_joining_existentials.v b/theories/barrier/example_joining_existentials.v
index 8bc57054..a27ee02f 100644
--- a/theories/barrier/example_joining_existentials.v
+++ b/theories/barrier/example_joining_existentials.v
@@ -13,7 +13,7 @@ Definition Shot {Σ} {F : oFunctor} (x : oFunctor_apply F (iPropO Σ)) : one_sho
   Cinr $ to_agree $ Next $ x.
 
 Class oneShotG (Σ : gFunctors) (F : oFunctor) :=
-  one_shot_inG :> inG Σ (one_shotR Σ F).
+  one_shot_inG :: inG Σ (one_shotR Σ F).
 Definition oneShotΣ (F : oFunctor) : gFunctors :=
   #[ GFunctor (csumRF (exclRF unitO) (agreeRF (â–¶ F))) ].
 Global Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
diff --git a/theories/barrier/proof.v b/theories/barrier/proof.v
index 148223e9..b81c2265 100644
--- a/theories/barrier/proof.v
+++ b/theories/barrier/proof.v
@@ -8,8 +8,8 @@ From iris.prelude Require Import options.
 
 (** The CMRAs/functors we need. *)
 Class barrierG Σ := BarrierG {
-  barrier_inG :> inG Σ (authR (gset_disjUR gname));
-  barrier_savedPropG :> savedPropG Σ;
+  barrier_inG :: inG Σ (authR (gset_disjUR gname));
+  barrier_savedPropG :: savedPropG Σ;
 }.
 Definition barrierΣ : gFunctors :=
   #[ GFunctor (authRF (gset_disjUR gname)); savedPropΣ ].
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 9d83ac54..3e294388 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -59,7 +59,7 @@ Definition pop : val :=
     end.
 
 Definition channelR := exclR unitR.
-Class channelG Σ := { channel_inG :> inG Σ channelR }.
+Class channelG Σ := { channel_inG :: inG Σ channelR }.
 Definition channelΣ : gFunctors := #[GFunctor channelR].
 Global Instance subG_channelΣ {Σ} : subG channelΣ Σ → channelG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 918989ec..b1ff313f 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -58,7 +58,7 @@ Definition pop : val :=
     end.
 
 Definition channelR := exclR unitR.
-Class channelG Σ := {channel_inG :> inG Σ channelR}.
+Class channelG Σ := {channel_inG :: inG Σ channelR}.
 
 Section proofs.
   Context `{!heapGS Σ, !channelG Σ} (N : namespace).
diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v
index 69c928ad..85c7070c 100644
--- a/theories/hocap/cg_bag.v
+++ b/theories/hocap/cg_bag.v
@@ -40,8 +40,8 @@ Definition popBag : val := λ: "b",
 
 Canonical Structure valmultisetO := leibnizO (gmultiset valO).
 Class bagG Σ := BagG
-{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
-  lock_bagG :> lockG Σ
+{ bag_bagG :: inG Σ (prodR fracR (agreeR valmultisetO));
+  lock_bagG :: lockG Σ
 }.
 
 (** Generic specification for the bag, using view shifts. *)
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index e3c0f949..acf475bc 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -15,7 +15,7 @@ From iris.prelude Require Import options.
     FIN v = the task has been completed with the result v *)
 (* We use this RA to verify the Task.run() method *)
 Definition saR := csumR fracR (csumR (prodR fracR (agreeR valO)) (agreeR valO)).
-Class saG Σ := { sa_inG :> inG Σ saR }.
+Class saG Σ := { sa_inG :: inG Σ saR }.
 Definition INIT `{saG Σ} γ (q: Qp) := own γ (Cinl q%Qp).
 Definition SET_RES `{saG Σ} γ (q: Qp) (v: val) := own γ (Cinr (Cinl (q%Qp, to_agree v))).
 Definition FIN `{saG Σ} γ (v: val) := own γ (Cinr (Cinr (to_agree v))).
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 3c348a3e..a3ea7b8a 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -36,7 +36,7 @@ Definition popBag : val := rec: "pop" "b" :=
 
 Canonical Structure valmultisetO := leibnizO (gmultiset valO).
 Class bagG Σ := BagG
-{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
+{ bag_bagG :: inG Σ (prodR fracR (agreeR valmultisetO));
 }.
 
 (** Generic specification for the bag, using view shifts. *)
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 05fc171a..dc4a5df8 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 (** We are going to need the oneshot RA to verify the
     Task.Join() method *)
 Definition oneshotR := csumR fracR (agreeR valO).
-Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+Class oneshotG Σ := { oneshot_inG :: inG Σ oneshotR }.
 Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
 Global Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index aec7ca2f..9fd075d6 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -9,7 +9,7 @@ From iris.prelude Require Import options.
 
 From iris_examples.lecture_notes Require Import modular_incr.
 
-Class ccounterG Σ := CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
+Class ccounterG Σ := CCounterG { ccounter_inG :: inG Σ (frac_authR natR) }.
 Definition ccounterΣ : gFunctors := #[GFunctor (frac_authR natR)].
 
 Global Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index b9eb89cd..c75a08b6 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -218,7 +218,7 @@ Section monotone_counter.
   (* We now need to tell Coq to use our RA as one of the RA's in the instantiation of Iris. *)
   (* This is achieved via the subG constructor. All of this is boilerplate, so
      the proofs are trivial, with the tactics provided by the library. *)
-  Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ mcounterRA }.
+  Class mcounterG Σ := MCounterG { mcounter_inG :: inG Σ mcounterRA }.
   Definition mcounterΣ : gFunctors := #[GFunctor mcounterRA].
   
   Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
@@ -410,7 +410,7 @@ Section monotone_counter'.
   (* We tell Coq that our Iris instantiation has the following resource
      algebras. Note that the only diffference from above is that we use authR
      max_natUR in place of the resource algebra mcounterRA we constructed above. *)
-  Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR max_natUR)}.
+  Class mcounterG' Σ := MCounterG' { mcounter_inG' :: inG Σ (authR max_natUR)}.
   Definition mcounterΣ' : gFunctors := #[GFunctor (authR max_natUR)].
 
   Global Instance subG_mcounterΣ' {Σ} : subG mcounterΣ' Σ → mcounterG' Σ.
@@ -549,7 +549,7 @@ Section ccounter.
   (* We start as we did before, telling Coq what we assume from the Iris instantiation. *)
   (* Note that now we use natR as the underlying resource algebra. This is the
      RA of natural numbers with addition as the operation. *)
-  Class ccounterG Σ := CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
+  Class ccounterG Σ := CCounterG { ccounter_inG :: inG Σ (frac_authR natR) }.
   Definition ccounterΣ : gFunctors := #[GFunctor (frac_authR natR)].
 
   Global Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index b1bc4d52..5d9a732a 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -28,7 +28,7 @@ From iris.algebra Require Import excl.
    projects, mostly with the goal of catching common mistakes. *)
 From iris.prelude Require Import options.
 
-Class lockG Σ := lock_G :> inG Σ (exclR unitR).
+Class lockG Σ := lock_G :: inG Σ (exclR unitR).
 
 Section lock_model.
 (* In order to do the proof we need to assume certain things about the
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 8ff6a39b..1f608317 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -12,7 +12,7 @@ From iris.heap_lang.lib Require Import par.
 
 Definition cntCmra : cmra := prodR fracR (agreeR ZO).
 
-Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
+Class cntG Σ := CntG { CntG_inG :: inG Σ cntCmra }.
 Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
 
 Global Instance subG_cntΣ {Σ} : subG cntΣ Σ → cntG Σ.
diff --git a/theories/lecture_notes/sfra.v b/theories/lecture_notes/sfra.v
index c7bbcf0f..7cb242e9 100644
--- a/theories/lecture_notes/sfra.v
+++ b/theories/lecture_notes/sfra.v
@@ -71,8 +71,8 @@ Proof.
   (* - done. *)
 Qed.
 
-Class SFG Σ := SF_G :> inG Σ (SFRA).
-Class FracG Σ := Frac_G :> inG Σ (fracR).
+Class SFG Σ := SF_G :: inG Σ (SFRA).
+Class FracG Σ := Frac_G :: inG Σ (fracR).
 
 End RADefinitions.
 
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index d19cfef7..d91eff4e 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -162,7 +162,7 @@ Section algebra.
   Global Instance sumRA_cmra_discrete : CmraDiscrete sumRA.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Class sumG Σ := SumG { sum_inG :> inG Σ sumRA }.
+  Class sumG Σ := SumG { sum_inG :: inG Σ sumRA }.
   Definition sumΣ : gFunctors := #[GFunctor sumRA].
 
   Global Instance subG_sumΣ {Σ} : subG sumΣ Σ → sumG Σ.
@@ -225,9 +225,9 @@ End array_model.
 
 (** The CMRAs we need. *)
 Class alockG Σ := {
-  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat)));
-  tlock_sumG :> sumG Σ;
-  tlock_tokenG :> inG Σ ((prodR (optionUR (exclR unitO)) (optionUR (exclR unitO))));
+  tlock_G :: inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat)));
+  tlock_sumG :: sumG Σ;
+  tlock_tokenG :: inG Σ ((prodR (optionUR (exclR unitO)) (optionUR (exclR unitO))));
 }.
 
 Section proof.
@@ -382,7 +382,7 @@ Section proof.
     { iNext. rewrite /lock_inv. iExists 0, 0, (<[0:=true]> (replicate cap false)).
       iFrame. iSplitR.
       - by rewrite insert_length replicate_length.
-      - iLeft. iFrame. rewrite Nat.mod_0_l //. lia. }
+      - iLeft. iFrame. rewrite Nat.Div0.mod_0_l //. }
     wp_pures.
     iApply "Post".
     rewrite /is_lock. iFrame.
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index 6afcd992..c16e6482 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -89,9 +89,9 @@ Definition tokenUR    := exclR unitO.
 Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
 
 Class cincG Σ := ConditionalIncrementG {
-                     cinc_numG      :> inG Σ numUR;
-                     cinc_tokenG    :> inG Σ tokenUR;
-                     cinc_one_shotG :> inG Σ one_shotUR;
+                     cinc_numG      :: inG Σ numUR;
+                     cinc_tokenG    :: inG Σ tokenUR;
+                     cinc_one_shotG :: inG Σ one_shotUR;
                    }.
 
 Definition cincΣ : gFunctors :=
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 220e3f97..a8b52a1a 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -65,12 +65,12 @@ End counter_impl.
 
 (** ** Ghost state for the counter *)
 Class counterG (Σ : gFunctors) := {
-  counter_nat_gname_mapG :> ghost_mapG Σ nat gname;
-  counter_nat_gnames_mapG :> ghost_mapG Σ nat (gname * gname);
-  counter_ghost_varG :> ghost_varG Σ bool;
-  counter_mono_natG :> mono_natG Σ;
-  counter_tokenG :> inG Σ (exclR unitO);
-  counter_ghost_setG :> ghost_mapG Σ (gname * gname) unit;
+  counter_nat_gname_mapG :: ghost_mapG Σ nat gname;
+  counter_nat_gnames_mapG :: ghost_mapG Σ nat (gname * gname);
+  counter_ghost_varG :: ghost_varG Σ bool;
+  counter_mono_natG :: mono_natG Σ;
+  counter_tokenG :: inG Σ (exclR unitO);
+  counter_ghost_setG :: ghost_mapG Σ (gname * gname) unit;
 }.
 
 Definition counterΣ : gFunctors :=
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index 885c1d77..d476906e 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -287,7 +287,7 @@ hocap_auth.stack_content_frag := frag
 
 (** The CMRA & functor we need. *)
 Class hocapG Σ := HocapG {
-  hocap_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
+  hocap_stateG :: inG Σ (authR (optionUR $ exclR (listO valO)));
 }.
 Definition hocapΣ : gFunctors :=
   #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 146a6c70..eae5d0b9 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -13,8 +13,8 @@ heap. *)
 (** The CMRA & functor we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
 Class stackG Σ := StackG {
-  stack_tokG :> inG Σ (exclR unitO);
-  stack_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
+  stack_tokG :: inG Σ (exclR unitO);
+  stack_stateG :: inG Σ (authR (optionUR $ exclR (listO valO)));
  }.
 Definition stackΣ : gFunctors :=
   #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v
index d1bfb6fc..b45dee42 100644
--- a/theories/logatom/flat_combiner/atomic_sync.v
+++ b/theories/logatom/flat_combiner/atomic_sync.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 (** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
 
 Definition syncR := prodR fracR (agreeR valO). (* track the local knowledge of ghost state *)
-Class syncG Σ := sync_tokG :> inG Σ syncR.
+Class syncG Σ := sync_tokG :: inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
 Global Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index d7afe15c..dd218292 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -52,9 +52,9 @@ Definition mk_flat : val :=
 Definition reqR := prodR fracR (agreeR valO). (* request x should be kept same *)
 Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
 Class flatG Σ := FlatG {
-  req_G :> inG Σ reqR;
-  sp_G  :> savedPredG Σ val;
-  tok_G :> inG Σ (exclR unitO);
+  req_G :: inG Σ reqR;
+  sp_G  :: savedPredG Σ val;
+  tok_G :: inG Σ (exclR unitO);
 }.
 
 Definition flatΣ : gFunctors :=
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 0aa9e761..5348b47c 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -120,10 +120,10 @@ Definition backUR := authR max_natUR.
 
 Class hwqG Σ :=
   HwqG {
-    hwq_arG   :> inG Σ eltsUR; (** Logical contents of the queue. *)
-    hwq_contG :> inG Σ contUR; (** One-shot for contradiction states. *)
-    hwq_slotG :> inG Σ slotUR; (** State data for used array slots. *)
-    hwq_back  :> inG Σ backUR; (** Used to show that back only increases. *)
+    hwq_arG   :: inG Σ eltsUR; (** Logical contents of the queue. *)
+    hwq_contG :: inG Σ contUR; (** One-shot for contradiction states. *)
+    hwq_slotG :: inG Σ slotUR; (** State data for used array slots. *)
+    hwq_back  :: inG Σ backUR; (** Used to show that back only increases. *)
   }.
 
 Definition hwqΣ : gFunctors :=
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 00dc678c..4050d8bc 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -158,9 +158,9 @@ Definition tokenUR    := exclR unitO.
 Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
 
 Class rdcssG Σ := RDCSSG {
-                     rdcss_valG      :> inG Σ valUR;
-                     rdcss_tokenG    :> inG Σ tokenUR;
-                     rdcss_one_shotG :> inG Σ one_shotUR;
+                     rdcss_valG      :: inG Σ valUR;
+                     rdcss_tokenG    :: inG Σ tokenUR;
+                     rdcss_one_shotG :: inG Σ one_shotUR;
                    }.
 
 Definition rdcssΣ : gFunctors :=
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 02f0625a..9152f90d 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -75,8 +75,8 @@ Definition read_with_proph : val :=
 Definition timestampUR := gmapUR Z $ agreeR valO.
 
 Class atomic_snapshotG Σ := AtomicSnapshotG {
-                                atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valO;
-                                atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
+                                atomic_snapshot_stateG :: inG Σ $ authR $ optionUR $ exclR $ valO;
+                                atomic_snapshot_timestampG :: inG Σ $ authR $ timestampUR
 }.
 Definition atomic_snapshotΣ : gFunctors :=
   #[GFunctor (authR $ optionUR $ exclR $ valO); GFunctor (authR timestampUR)].
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index 84afa0ef..d67cd99a 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -59,7 +59,7 @@ Definition pop_stack : val :=
 (** * Definition of the required camera *************************************)
 
 Class stackG Σ := StackG {
-  stack_tokG :> inG Σ (authR (optionUR (exclR (listO valO)))) }.
+  stack_tokG :: inG Σ (authR (optionUR (exclR (listO valO)))) }.
 
 Definition stackΣ : gFunctors :=
   #[GFunctor (authR (optionUR (exclR (listO valO))))].
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 08e0d8bd..929d354a 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -25,7 +25,7 @@ Definition to_heap {L V} `{Countable L} : gmap L V → heapUR L V :=
   fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
 
 (** The CMRA for the thread pool. *)
-Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
+Class cfgSG Σ := CFGSG { cfg_inG :: inG Σ (authR cfgUR); cfg_name : gname }.
 
 Section definitionsS.
   Context `{cfgSG Σ, invGS Σ}.
diff --git a/theories/logrel/F_mu_ref_conc/unary/soundness.v b/theories/logrel/F_mu_ref_conc/unary/soundness.v
index a039597b..b90c6e46 100644
--- a/theories/logrel/F_mu_ref_conc/unary/soundness.v
+++ b/theories/logrel/F_mu_ref_conc/unary/soundness.v
@@ -4,8 +4,8 @@ From iris.program_logic Require Import adequacy.
 From iris.prelude Require Import options.
 
 Class heapPreIG Σ := HeapPreIG {
-  heap_preG_iris :> invGpreS Σ;
-  heap_preG_heap :> gen_heapGpreS loc F_mu_ref_conc.val Σ
+  heap_preG_iris :: invGpreS Σ;
+  heap_preG_heap :: gen_heapGpreS loc F_mu_ref_conc.val Σ
 }.
 
 Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
diff --git a/theories/logrel/F_mu_ref_conc/wp_rules.v b/theories/logrel/F_mu_ref_conc/wp_rules.v
index f12f7ad1..f180433b 100644
--- a/theories/logrel/F_mu_ref_conc/wp_rules.v
+++ b/theories/logrel/F_mu_ref_conc/wp_rules.v
@@ -11,7 +11,7 @@ From iris.prelude Require Import options.
     physical heap. *)
 Class heapIG Σ := HeapIG {
   heapI_invG : invGS Σ;
-  heapI_gen_heapG :> gen_heapGS loc val Σ;
+  heapI_gen_heapG :: gen_heapGS loc val Σ;
 }.
 
 Global Instance heapIG_irisG `{heapIG Σ} : irisGS F_mu_ref_conc_lang Σ := {
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index 6352c14b..fd68ebcd 100644
--- a/theories/spanning_tree/mon.v
+++ b/theories/spanning_tree/mon.v
@@ -21,9 +21,9 @@ Definition markingUR : ucmra := gsetUR loc.
 (** The CMRA we need. *)
 Class graphG Σ := GraphG
   {
-    graph_marking_inG :> inG Σ (authR markingUR);
+    graph_marking_inG :: inG Σ (authR markingUR);
     graph_marking_name : gname;
-    graph_inG :> inG Σ (authR graphUR);
+    graph_inG :: inG Σ (authR graphUR);
     graph_name : gname
   }.
 (** The Functor we need. *)
@@ -70,7 +70,7 @@ Definition Gmon := gmapR loc (exclR chlO).
 Definition excl_chlC_chl (ch : exclR chlO) : option (option loc * option loc) :=
   match ch with
   | Excl w => Some w
-  | Excl_Bot => None
+  | ExclBot => None
   end.
 
 Definition Gmon_graph (G : Gmon) : graph loc := omap excl_chlC_chl G.
-- 
GitLab