diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 7ea33f076ef2ee264da84a6ba65ac5c20660720a..05315b8ca366ec038cd967817a2f899ded151084 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -17,8 +17,8 @@ Definition lrustΣ : gFunctors :=
 Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
-  (∀ `{lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
+  (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
   adequate NotStuck e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 590b23f7f48e36ad1456b60d7fd836b1ca6a2ce9..38b1406200ed9089d7b1cd97e742a9b70a94d31b 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
     qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
 
 Section definitions.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
 
   Definition heap_mapsto_st (st : lock_state)
              (l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -106,7 +106,7 @@ Section to_heap.
 End to_heap.
 
 Section heap.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types σ : state.
   Implicit Types E : coPset.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index cd64baa245f76e4c1fa06e997840c6e782820f2b..c302a1c3cd70ba189f75aab431796d9ad51a9fbf 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -91,7 +91,7 @@ Proof. rewrite /Closed. apply _. Qed.
 
 Inductive val :=
 | LitV (l : base_lit)
-| RecV (f : binder) (xl : list binder) (e : expr) `{Closed (f :b: xl +b+ []) e}.
+| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
 
 Bind Scope val_scope with val.
 
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 6cf5ee8c68e953404f7ab9125012d745b425dce1..1897f020e25751f64a39df1e73e65da12b039285 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (at level 80, n, i at next level,
    format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 1feb16e7e3eaf55e8709486fa5807c72457e2eba..6a4be069df2e8d00a919f3c3f73d943e936ed092 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -13,7 +13,7 @@ Definition delete : val :=
     else Free "n" "loc".
 
 Section specs.
-  Context `{lrustG Σ}.
+  Context `{!lrustG Σ}.
 
   Lemma wp_new E n:
     0 ≤ n →
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 8550d80be55b34c74c4994d76f27bd9e2bd5082f..d182c900cf72ad3248326c888b4343540b8c047b 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
          "p2" <- "x";;
          "swap" ["p1" +â‚— #1 ; "p2" +â‚— #1 ; "len" - #1].
 
-Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
     swap [ #l1; #l2; #n] @ E
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 2da5f05eb6849d61538c86685326918cf26af522..4bac769097151f753dddbf74c9c84638fac99ab6 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -11,7 +11,7 @@ Class lrustG Σ := LRustG {
   lrustG_gen_heapG :> heapG Σ
 }.
 
-Instance lrustG_irisG `{lrustG Σ} : irisG lrust_lang Σ := {
+Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
   iris_invG := lrustG_invG;
   state_interp σ κs _ := heap_ctx σ;
   fork_post _ := True%I;
@@ -61,7 +61,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
 Proof. by rewrite /DoSubstL subst_v_eq. Qed.
 
 Section lifting.
-Context `{lrustG Σ}.
+Context `{!lrustG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types e : expr.
 Implicit Types ef : option expr.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 4abc2eaadd41f86ed351926f10afce2540d5252c..a1b3db3e1a85ef863601d8ab98f9845d350230d5 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From iris.program_logic Require Import lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
 
-Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
-Lemma tac_wp_eq_loc `{lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
   envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
 Tactic Notation "wp_if" := wp_pure (If _ _ _).
 Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
 
-Lemma tac_wp_bind `{lrustG Σ} K Δ E Φ e :
+Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
@@ -89,7 +89,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   end.
 
 Section heap.
-Context `{lrustG Σ}.
+Context `{!lrustG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 3373c818dd6ccfd67e3209f9ba9c4060380bbfe2..e982eb17f35565d4c991a6545538e5630f1f456e 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{!invG Σ, !lftG Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
+  Context `{!invG Σ, !lftG Σ} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 489ed417f683c52a75f19842e462d5b25af28e3f..e844bbda3abfce60326e2c44efcbaa205123d768 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -7,13 +7,13 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
                        (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ'])))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -112,7 +112,7 @@ Section frac_bor.
       iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
   Qed.
 
-  Lemma frac_bor_acc E q κ `{Fractional _ φ} :
+  Lemma frac_bor_acc E q κ `{!Fractional φ} :
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
@@ -134,7 +134,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 735ae6d1c528afce6c9c17addc0c685d4e686058..fe1429b756ff7c8a0f62cbf6b4057ecd2837b3a5 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -23,7 +23,7 @@ Instance lft_inhabited : Inhabited lft := populate static.
 Canonical lftC := leibnizC lft.
 
 Section derived.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma bor_acc_atomic_cons E κ P :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index fe4827cdddc386968b8e98e10a184271da9aa314..eb1d9569f06d00688644e1b92b0b9b014fa9d52d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -23,17 +23,17 @@ Module Type lifetime_sig.
   Parameter static : lft.
   Parameter lft_intersect : lft → lft → lft.
 
-  Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
 
-  Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
-  Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
+  Parameter lft_tok : ∀ `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{!lftG Σ} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
-  Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
@@ -47,7 +47,7 @@ Module Type lifetime_sig.
   Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
 
   Section properties.
-  Context `{invG, lftG Σ}.
+  Context `{!invG Σ, !lftG Σ}.
 
   (** Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -155,6 +155,6 @@ Module Type lifetime_sig.
   Parameter lftΣ : gFunctors.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
-  Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
+  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
     (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
 End lifetime_sig.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 0cd3d78d6e0ce93d6a18da066f66b51ef04d844c..573c445693d8dc84273e5695db86b3bb9c4706bd 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 8138b837bb99d948c8d83c1393c749c513f89e19..03ff321de45284ee6170d7c1f25ceb01f33b93e7 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 45ba12f1c639c29461594cb072f98291bd21ed2e..70b98634a788feb1d7719f59e7d6c81dedc55aef 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 152af54861d89d70007a3f1b419d52cf61d62014..9c3364432bfa526c35a6c0c261c2ad5bb936c8e6 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index ae52a295ecea8a345fd4e50e11455266f7cb1194..8342a18c3b160accea5d9bc8b5a0ee784940f08d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -79,7 +79,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
 
 Section defs.
-  Context `{invG Σ, lftG Σ}.
+  Context `{!invG Σ, !lftG Σ}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -224,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 4dcbb159bd5afa1a17f96643d29e37bbd9fe120f..decf7ad3365dc6db755aa6cf0fb5913dd350a51e 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 19ca418de968ba94d41eac81ba5ecad6aed10cf0..c633f1dd66ab73ef976220e7bbce4ea4c48b107c 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section primitive.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index b0c84dd1c121a395969f8d0a0ba7d3d169f6fe39..d7e2e4b09e6450515dbfa576c126f06b218dae41 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 415516877fa114e66db68a468321a91b5eb9bc16..7af98c9eb5873dd58d932cf5ff0cd9e6eae75e0d 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
+Definition na_bor `{!invG Σ, !lftG Σ, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{invG Σ, lftG Σ, na_invG Σ}
+  Context `{!invG Σ, !lftG Σ, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 4a4d6a15b0336f088fb9a0e3b427528b7b835378..3375a9cb99da512ad3cc75b5c482c1dadacfc8e0 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section bool.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition bool : type :=
     {| st_own tid vl :=
@@ -22,7 +22,7 @@ Section bool.
 End bool.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 6ab6044295b8b3630bc340114b51fec622c9eb5a..7557c5de306db4f6f20c88844e24db6fd8be4a2b 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
   concurrently. *)
 
 Section borrow.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 02ef7650e5508e4fca52969098380e70c59eee2f..1011aa9412071ff20563a91c0ab864cedb2b519a 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
   Lemma type_jump args argsv E L C T k T' :
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index a86297a4794aea8a71e6c4dd27cc6f12dc44fd12..c29c7315063f891ea86509fc6027ddc1d10d6997 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
 
 Section cont_context_def.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition cont_postcondition : iProp Σ := True%I.
 
@@ -20,7 +20,7 @@ Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T)
   (at level 70, format "k  ◁cont( L ,  T )").
 
 Section cont_context.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
     let '(k ◁cont(L, T)) := x in
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 3052ba5a7a8f0be9d049654bb3f02baa2939c751..e71c3dec260514be8d18f2b234a2a43721bd6b14 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section get_x.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition get_x : val :=
     funrec: <> ["p"] :=
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 77b4de9189d541f1890ffd314e21a4a723a865e3..49723aed3f84344b24a50a573f2f487dd01c541f 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section init_prod.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition init_prod : val :=
     funrec: <> ["x"; "y"] :=
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 1efdcf94ca0c6a81ef5b82111e9f52d17b498fd8..0bc054bcd7d9a7c3c67526be656eb62bb8d7d7b2 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section lazy_lft.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition lazy_lft : val :=
     funrec: <> [] :=
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 6510eff842a4cf5f685896e2b84453363100d981..2666af36b38fb2ea633de568ec99da47b5bde83b 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -13,7 +13,7 @@ From lrust.typing Require Import typing lib.option.
 *)
 
 Section non_lexical.
-  Context `{typeG Σ} (HashMap K V : type)
+  Context `{!typeG Σ} (HashMap K V : type)
           `{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
           (defaultv get_mut insert: val).
 
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index c8b0b12783079550d086e9b1006c0f88b73314bc..e761beeb3d62047f761a90f43a69f9107a5220c5 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section rebor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition rebor : val :=
     funrec: <> ["t1"; "t2"] :=
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index cb63526d34ebc2b63732a86702ea240a95562378..b27bbd923d18e086ba95a3e7ab0244201fd88a19 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unbox.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition unbox : val :=
     funrec: <> ["b"] :=
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index f93012b0002611a21f60bb66813273680f035b24..58a14e00c32827fbe854262994200ffb67644a89 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section fixpoint_def.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance type_inhabited : Inhabited type := populate bool.
@@ -25,7 +25,7 @@ Section fixpoint_def.
      I believe this gives the right sets for all types that we can define in
      Rust, but I do not have any proof of this.
      TODO : investigate this in more detail. *)
-  Global Instance type_fixpoint_wf `{∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
+  Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
     let lfts :=
       let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
       (T type_fixpoint).(ty_lfts)
@@ -37,13 +37,13 @@ Section fixpoint_def.
     {| ty_lfts := lfts; ty_wf_E := wf_E |}.
 End fixpoint_def.
 
-Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
+Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
     `{!TypeContractive T1, !TypeContractive T2} n :
   (∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
 Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
 
 Section fixpoint.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Context (T : type → type) {HT: TypeContractive T}.
 
   Global Instance fixpoint_copy :
@@ -98,7 +98,7 @@ Section fixpoint.
 End fixpoint.
 
 Section subtyping.
-  Context `{typeG Σ} (E : elctx) (L : llctx).
+  Context `{!typeG Σ} (E : elctx) (L : llctx).
 
   (* TODO : is there a way to declare these as a [Proper] instances ? *)
   Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
@@ -114,7 +114,7 @@ Section subtyping.
       apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
+  Lemma fixpoint_proper T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
     (∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
     eqtype E L (type_fixpoint T1) (type_fixpoint T2).
   Proof.
@@ -127,16 +127,16 @@ Section subtyping.
         apply bi.limit_preserving_entails; solve_proper.
   Qed.
 
-  Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_subtype_l ty T `{!TypeContractive T} :
     subtype E L ty (T (type_fixpoint T)) → subtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_subtype_r ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_subtype_r ty T `{!TypeContractive T} :
     subtype E L (T (type_fixpoint T)) ty → subtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_l ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_eqtype_l ty T `{!TypeContractive T} :
     eqtype E L ty (T (type_fixpoint T)) → eqtype E L ty (type_fixpoint T).
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
-  Lemma fixpoint_unfold_eqtype_r ty T `{TypeContractive T} :
+  Lemma fixpoint_unfold_eqtype_r ty T `{!TypeContractive T} :
     eqtype E L (T (type_fixpoint T)) ty → eqtype E L (type_fixpoint T) ty.
   Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
 End subtyping.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 73aed28266188edaf80c9d43814d1990583701bd..6fe52645302722f1c775e52b2f1b0124fb537409 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import own programs cont.
 Set Default Proof Using "Type".
 
 Section fn.
-  Context `{typeG Σ} {A : Type} {n : nat}.
+  Context `{!typeG Σ} {A : Type} {n : nat}.
 
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
@@ -141,7 +141,7 @@ Notation "'fn(' E ')' '→' R" :=
 Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
     (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
@@ -390,7 +390,7 @@ Section typing.
   Qed.
 
   Lemma type_rec {A} E L fb (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
     IntoVal ef (funrec: fb argsb := e) →
     n = length argsb →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
@@ -413,7 +413,7 @@ Section typing.
   Qed.
 
   Lemma type_fn {A} E L (argsb : list binder) ef e n
-        (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+        (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
     IntoVal ef (funrec: <> argsb := e) →
     n = length argsb →
     □ (∀ x ϝ k (args : vec val (length argsb)),
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 5f94433c1935aec43dcbe14f62db55d93e8ef9c8..0b3d8e1cf9a5d359ea89ab29d4c2cdff9bfdc8ca 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import bool programs.
 Set Default Proof Using "Type".
 
 Section int.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition int : type :=
     {| st_own tid vl :=
@@ -22,7 +22,7 @@ Section int.
 End int.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 1291369424c080fc27f4fe79cd15820b747aa254..eead3bd411a37cf215e727badb32e041804fb718 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -22,7 +22,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{invG Σ, lftG Σ}.
+  Context `{!invG Σ, !lftG Σ}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -308,7 +308,7 @@ Arguments elctx_sat {_ _ _} _ _ _.
 Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index dea59d49a8641bf1d121dd0989bdc690eae76301..c3c800273fb64179782f3f1c2734379fc360b1e0 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section cell.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
@@ -79,7 +79,7 @@ Section cell.
 End cell.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** The next couple functions essentially show owned-type equalities, as they
       are all different types for the identity function. *)
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 7d50663f8ace14141594620c0424bd675ae1162b..384b44cf7e33b0d37a6b5a85eb4f0effa9c02981 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section fake_shared.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition fake_shared_box : val :=
     funrec: <> ["x"] := Skip ;; return: ["x"].
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 8ac02855e498e77614ddcd504365133fb0783a25..b7d0b2fd5ed038782bf65f517db52866c20dafd3 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing lib.panic.
 Set Default Proof Using "Type".
 
 Section option.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 5296c6c4c7ac7d9d63548977860c605295f10dc2..f6a6b094f87a94a6605e424d6cdb27f7ab83d584 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
    [take_mut]. *)
 
 Section panic.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition panic : val :=
     funrec: <> [] := #☠.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 91852456608624b158f351141fe1a11f4d7c0552..6f403685929c2415cb193e6d41a2f0b4c636bc1d 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Definition refcell_refN := refcellN .@ "ref".
 
 Section ref.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index b791f6054251fbb13c0df8de4639c0a443f93c63..181d9dde4231d48afd1569f28c9b36b9fb75132f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell ref.
 Set Default Proof Using "Type".
 
 Section ref_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   Lemma refcell_inv_reading_inv tid l γ α ty q ν :
     refcell_inv tid l γ α ty -∗
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index f8ad34958d20aa16ea625eeb6bd091c2cf6187b1..ebb22ebaa14bd2a1725246884ba2e7dfca9a4858 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -40,7 +40,7 @@ Definition refcellN := lrustN .@ "refcell".
 Definition refcell_invN := refcellN .@ "inv".
 
 Section refcell_inv.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
     (∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (● (refcell_st_to_R st)) ∗
@@ -94,7 +94,7 @@ Section refcell_inv.
 End refcell_inv.
 
 Section refcell.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Original Rust type:
      pub struct RefCell<T: ?Sized> {
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 8c10eb20b72ef127160f448f222079b337c022f8..a70435daeeea57c643fc82552c3f9fd724724f4b 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -9,7 +9,7 @@ From lrust.typing.lib.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
 Section refcell_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Constructing a refcell. *)
   Definition refcell_new ty : val :=
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index a00a34f98b3b31373c182a23970975fdd15c1a3f..c8e0f46c6c440e868f5ae5471aeca8891a37bfd9 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Section refmut.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* The Rust type looks as follows (after some unfolding):
 
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index fa5374c6f7a824adde5b612b6536848b9ec7fd2a..719970bd442560d8103510fca3b35726a69e5c19 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell refmut.
 Set Default Proof Using "Type".
 
 Section refmut_functions.
-  Context `{typeG Σ, refcellG Σ}.
+  Context `{!typeG Σ, !refcellG Σ}.
 
   (* Turning a refmut into a shared borrow. *)
   Definition refmut_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 2ee4f34a7428d4fcc35da1b2684d69753ef44bfe..4d4e1a472f1a6c865999f0856c8d7a013ec79872 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -28,7 +28,7 @@ Definition writing_st : rwlock_stR :=
 Definition rwlockN := lrustN .@ "rwlock".
 
 Section rwlock_inv.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   Definition rwlock_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
     (∃ st, l ↦ #(Z_of_rwlock_st st) ∗ own γ (● st) ∗
@@ -83,7 +83,7 @@ Section rwlock_inv.
 End rwlock_inv.
 
 Section rwlock.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
      pub struct RwLock<T: ?Sized> {
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2287685651a262131e3f115fc24bdb0a6f698124..964ecea96fc47cdbd95eea30cf5a11f59f3123cc 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -9,7 +9,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
 Set Default Proof Using "Type".
 
 Section rwlock_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Constructing a rwlock. *)
   Definition rwlock_new ty : val :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 692a354e1392429038cec136360129c51abecb90..e8878646dba13575507654a427e06dc0eca1dd6c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type:
     pub struct RwLockReadGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index c0e61e1bb822c87b52e83aaf8ffef7cf6a6bee7a..fccc7cea67ba6ebde98f749712bd09606c827129 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Turning a rwlockreadguard into a shared borrow. *)
   Definition rwlockreadguard_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index e48927ad15d208424985b9ac1dc47dcffec611c9..ef2e9d2b924a6c66d9a23f3ceb3ef7ba11f6689b 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Original Rust type (we ignore poisoning):
       pub struct RwLockWriteGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 9b15a6c80fd4a2b6794a03848298a243a24c76f4..b9c9010aa835b33b496cda96571a4e83ef6f6e5f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard_functions.
-  Context `{typeG Σ, rwlockG Σ}.
+  Context `{!typeG Σ, !rwlockG Σ}.
 
   (* Turning a rwlockwriteguard into a shared borrow. *)
   Definition rwlockwriteguard_deref : val :=
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index b1aef757d38e7040ad1651760374ead4f169c0fd..2b631d86e26b58ef14952deccbfda3bd703e3ac1 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -4,7 +4,7 @@ From lrust.lang.lib Require Import swap.
 Set Default Proof Using "Type".
 
 Section swap.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition swap ty : val :=
     funrec: <> ["p1"; "p2"] :=
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 2e075ad5b9fa01ddd6594bc4b1f846fa6a5dda41..b051af66cfa59584329e51ec01513c88e7578b6f 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section code.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition take ty (call_once : val) : val :=
     funrec: <> ["x"; "f"] :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c3c8dcfc5051a6c45800d71e094744be547e31ae..7280e94c066d27dce09f30ca1eca130d0958e0bd 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
 
 Section own.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
     match sz, n return _ with
@@ -147,7 +147,7 @@ Section own.
 End own.
 
 Section box.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Definition box ty := own_ptr ty.(ty_size) ty.
 
@@ -184,7 +184,7 @@ Section box.
 End box.
 
 Section util.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma ownptr_own n ty tid v :
     (own_ptr n ty).(ty_own) tid [v] ⊣⊢
@@ -215,7 +215,7 @@ Section util.
 End util.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index fbc9fdfbb1eba280c9a4b127777c11647b71e880..7076ceaae8e3dc8c6ebc21a5d24b56a8c2fb7f4a 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section product.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* TODO: Find a better spot for this. *)
   Lemma Z_nat_add (n1 n2 : nat) : Z.to_nat (n1 + n2) = (n1 + n2)%nat.
@@ -195,7 +195,7 @@ End product.
 Notation Π := product.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
   Proof.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 8130c5aedd2385fd4650d2049abb323c4aec0821..ac4177678019c775375159806cad513006c954ec 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import type_context lft_contexts product own uniq_bor
 Set Default Proof Using "Type".
 
 Section product_split.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** General splitting / merging for pointer types *)
   Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5a298fa46afc71aec62e1a78a1ce1acc683efcab..a5bea9a88a105d7bf03ec1cabecaa020427791e5 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Function Body *)
   (* This is an iProp because it is also used by the function type. *)
@@ -77,17 +77,17 @@ Section typing.
   Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
-Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
-Definition typed_val `{typeG Σ} (v : val) (ty : type) : Prop :=
+Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
 Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index b3a58cbf69bc02be96e2b7b3723c217666c9a9f9..4a4474512df53b38315dc78daf98558ff28f334d 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section shr_bor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
     {| st_own tid vl :=
@@ -60,7 +60,7 @@ End shr_bor.
 Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 096937a631861b0c65785e2c295ffccba4b799d4..84f4c4d382bb686c605dcc18151cce71166b005b 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -22,10 +22,10 @@ Proof. solve_inG. Qed.
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #☠.
 
-  Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
+  Definition main_type `{!typeG Σ} := (fn(∅) → unit)%T.
 
-  Theorem type_soundness `{typePreG Σ} (main : val) σ t :
-    (∀ `{typeG Σ}, typed_val main main_type) →
+  Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
+    (∀ `{!typeG Σ}, typed_val main main_type) →
     rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
     nonracing_threadpool t σ ∧
     (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
@@ -60,7 +60,7 @@ End type_soundness.
 (* Soundness theorem when no other CMRA is needed. *)
 
 Theorem type_soundness_closed (main : val) σ t :
-  (∀ `{typeG typeΣ}, typed_val main main_type) →
+  (∀ `{!typeG typeΣ}, typed_val main main_type) →
   rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
   nonracing_threadpool t σ ∧
   (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 97b9abfa3b2e0fcd8d4263395bc182d39d88154e..2e69050734f921dc6cb0e941147a1701b59fb994 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
 Section sum.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* We define the actual empty type as being the empty sum, so that it is
      convertible to it---and in particular, we can pattern-match on it
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 88a28ae56fa8ea108111274a5316357d3fdef34c..9f2a0c372d5710b87a217bd3435ab3cc8f6f22ca 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -18,7 +18,7 @@ Definition shrN  := lrustN .@ "shr".
 
 Definition thread_id := na_inv_pool_name.
 
-Record type `{typeG Σ} :=
+Record type `{!typeG Σ} :=
   { ty_size : nat;
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lft → thread_id → loc → iProp Σ;
@@ -52,14 +52,14 @@ Instance: Params (@ty_shr) 2 := {}.
 
 Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
-Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
 Arguments ty_wf_E {_ _} _ {_}.
 
-Definition ty_outlives_E `{typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
 
-Lemma ty_outlives_E_elctx_sat `{typeG Σ} E L ty `{!TyWf ty} α β :
+Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
   ty_outlives_E ty β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (ty_outlives_E ty α).
@@ -73,34 +73,34 @@ Proof.
 Qed.
 
 (* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive TyWfLst `{typeG Σ} : list type → Type :=
+Inductive TyWfLst `{!typeG Σ} : list type → Type :=
 | tyl_wf_nil : TyWfLst []
 | tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
 Existing Class TyWfLst.
 Existing Instances tyl_wf_nil tyl_wf_cons.
 
-Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty.(ty_lfts)
   | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
-Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty.(ty_wf_E)
   | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
-Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
   match WF with
   | tyl_wf_nil => []
   | tyl_wf_cons ty [] => ty_outlives_E ty κ
   | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
-Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
   tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl_outlives_E tyl α).
@@ -112,14 +112,14 @@ Proof.
       (etrans; [|done]); solve_typing.
 Qed.
 
-Record simple_type `{typeG Σ} :=
+Record simple_type `{!typeG Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
-Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
+Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
      (* [st.(st_own) tid vl] needs to be outside of the fractured
          borrow, otherwise I do not know how to prove the shr part of
@@ -148,7 +148,7 @@ Bind Scope lrust_type_scope with type.
 
 (* OFE and COFE structures on types and simple types. *)
 Section ofe.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Inductive type_equiv' (ty1 ty2 : type) : Prop :=
     Type_equiv :
@@ -259,7 +259,7 @@ End ofe.
 
 (** Special metric for type-nonexpansive and Type-contractive functions. *)
 Section type_dist2.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* Size and shr are n-equal, but own is only n-1-equal.
      We need this to express what shr has to satisfy on a Type-NE-function:
@@ -327,7 +327,7 @@ Notation TypeNonExpansive T := (∀ n, Proper (type_dist2 n ==> type_dist2 n) T)
 Notation TypeContractive T := (∀ n, Proper (type_dist2_later n ==> type_dist2 n) T).
 
 Section type_contractive.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma type_ne_dist_later T :
     TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
@@ -388,7 +388,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
   | S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1%nat) n
   end.
 
-Class Copy `{typeG Σ} (t : type) := {
+Class Copy `{!typeG Σ} (t : type) := {
   copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
     lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
@@ -401,34 +401,34 @@ Class Copy `{typeG Σ} (t : type) := {
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2 := {}.
 
-Class LstCopy `{typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
 Instance: Params (@LstCopy) 2 := {}.
-Global Instance lst_copy_nil `{typeG Σ} : LstCopy [] := List.Forall_nil _.
-Global Instance lst_copy_cons `{typeG Σ} ty tys :
+Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{!typeG Σ} ty tys :
   Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Send `{typeG Σ} (t : type) :=
+Class Send `{!typeG Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 Instance: Params (@Send) 2 := {}.
 
-Class LstSend `{typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
 Instance: Params (@LstSend) 2 := {}.
-Global Instance lst_send_nil `{typeG Σ} : LstSend [] := List.Forall_nil _.
-Global Instance lst_send_cons `{typeG Σ} ty tys :
+Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{!typeG Σ} ty tys :
   Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
 
-Class Sync `{typeG Σ} (t : type) :=
+Class Sync `{!typeG Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
 Instance: Params (@Sync) 2 := {}.
 
-Class LstSync `{typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
 Instance: Params (@LstSync) 2 := {}.
-Global Instance lst_sync_nil `{typeG Σ} : LstSync [] := List.Forall_nil _.
-Global Instance lst_sync_cons `{typeG Σ} ty tys :
+Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{!typeG Σ} ty tys :
   Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
 
 Section type.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (** Copy types *)
   Lemma shr_locsE_shift l n m :
@@ -519,24 +519,24 @@ Section type.
   Qed.
 End type.
 
-Definition type_incl `{typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
 Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
-Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
-Definition eqtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
 Instance: Params (@eqtype) 4 := {}.
 
 Section subtyping.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Global Instance type_incl_ne : NonExpansive2 type_incl.
   Proof.
@@ -670,7 +670,7 @@ Section subtyping.
 End subtyping.
 
 Section type_util.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma heap_mapsto_ty_own l ty tid :
     l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index bc169ec81ba45bc69336e38cb2218179ef24708e..e56f40dfc4869c53ef5e2ea7b8dd873babba9e3f 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -7,7 +7,7 @@ Bind Scope expr_scope with path.
 
 (* TODO: Consider making this a pair of a path and the rest. We could
    then e.g. formulate tctx_elt_hasty_path more generally. *)
-Inductive tctx_elt `{typeG Σ} : Type :=
+Inductive tctx_elt `{!typeG Σ} : Type :=
 | TCtx_hasty (p : path) (ty : type)
 | TCtx_blocked (p : path) (κ : lft) (ty : type).
 
@@ -18,7 +18,7 @@ Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
    (at level 70, format "p  ◁{ κ }  ty").
 
 Section type_context.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
   Implicit Types T : tctx.
 
   Fixpoint eval_path (p : path) : option val :=
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index c4fceaeee2830f4a001eac70a81ed319a462a3d5..cf00d06cf58693836246abbd8b808fb4189bf465 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
 
 Section case.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   (* FIXME : have a iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 28875d508995b63e6d3007e02a4a93a2b9c9e463..214c359f1aaae06ac98b3463810d04a8ae4a4a0f 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import product.
 Set Default Proof Using "Type".
 
 Section uninit.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition uninit_1 : type :=
     {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0b6923afecd832ab6ab53bfd07b122fc5e383e08..d796d3f8419da8c130d9c4720642dc016d89cec8 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import util lft_contexts type_context programs.
 Set Default Proof Using "Type".
 
 Section uniq_bor.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
@@ -98,7 +98,7 @@ End uniq_bor.
 Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
 
 Section typing.
-  Context `{typeG Σ}.
+  Context `{!typeG Σ}.
 
   Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
     lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →