diff --git a/tests/algebra.v b/tests/algebra.v
index cc94ecc7218f41cf270242e32d8255cc611c9a8e..028272cea5e582c85243c312e6582241c13e5648 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Import invariants.
 
 Section tests.
-  Context `{invG Σ}.
+  Context `{!invG Σ}.
 
   Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
     λne P v, (▷ (P v))%I.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 4a88fed5e105a649a4bf3022ac3dba5191bcfe1f..cd621a876f44085f36d2c1df4a5efe1c8daf0c2c 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -1,7 +1,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   E : coPset
   ============================
   --------------------------------------∗
@@ -10,7 +10,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   E : coPset
   l : loc
   ============================
@@ -21,7 +21,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   E : coPset
   l : loc
   ============================
@@ -35,7 +35,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   l : loc
   ============================
   _ : ▷ l ↦ #0
@@ -45,7 +45,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   l : loc
   ============================
   _ : l ↦ #1
@@ -55,7 +55,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   l : loc
   ============================
   "Hl1" : l ↦{1 / 2} #0
@@ -66,7 +66,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   l : loc
   ============================
   --------------------------------------∗
@@ -81,7 +81,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   ============================
   --------------------------------------∗
   WP "x" {{ _, True }}
@@ -89,7 +89,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
@@ -101,7 +101,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   ============================
@@ -114,7 +114,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
   Φ : language.val heap_lang → iPropI Σ
   E : coPset
@@ -128,7 +128,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
   ============================
   {{{ True }}}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index a738ffb97c32a3e87f15a21b94e80259c7d9e4a4..69c99fab2baa525bc758bc63a3d150951dd87b50 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -6,7 +6,7 @@ Set Ltac Backtrace.
 Set Default Proof Using "Type".
 
 Section tests.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val → iProp Σ.
 
@@ -147,7 +147,7 @@ Section tests.
 End tests.
 
 Section printing_tests.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
 
   (* These terms aren't even closed, but that's not what this is about.  The
   length of the variable names etc. has been carefully chosen to trigger
@@ -192,7 +192,7 @@ Section printing_tests.
 End printing_tests.
 
 Section error_tests.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
 
   Check "not_cas".
   Lemma not_cas :
diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index eb393dc0109ff2fbbf477951c30394bcf4b64a39..73cfb45d336fd9ea12cad338636bc4b649d44d26 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,7 +1,7 @@
 1 subgoal
   
   Σ : gFunctors
-  H : heapG Σ
+  heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
   ============================
   --------------------------------------∗
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index cada4949b06fb7ee6b4cf5af28a33d273660c745..f2e7050b08a79b9d03455054de061461006401a5 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 Section printing_tests.
-  Context `{heapG Σ}.
+  Context `{!heapG Σ}.
 
   Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
     True -∗ WP let: "val1" := fun1 #() in
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index abd2b0549d07a60a6ed7070d6aff07d1c330da73..7dcf6bde7a50056b557a72b1d901a08eb7872ab6 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -107,7 +107,7 @@ under max can be found in [theories/heap_lang/lib/counter.v]. *)
 update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
-Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
+Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
   nclose N ⊆ E → Atomic WeaklyAtomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index be465b628aea7e81b7222f6543d2bbe88eb977a0..b9a27dc9eb3129d554629394d5179e5117e133bd 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -131,7 +131,7 @@ Tactic failure: iFrame: cannot frame Q.
 1 subgoal
   
   PROP : sbi
-  H : BiAffine PROP
+  BiAffine0 : BiAffine PROP
   P, Q : PROP
   ============================
   _ : â–¡ P
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 981242fe35063e31a625547e3a3e329877e5493e..c5689c2ebd7f95e13e309044da68525ba1bdd0c4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -69,7 +69,7 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
   Q ∗ (Q -∗ P) -∗ P.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
 
-Lemma test_iDestruct_intuitionistic_affine_bi `{BiAffine PROP} P Q `{!Persistent P}:
+Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
 
@@ -180,7 +180,7 @@ Lemma test_iFrame_conjunction_2 P Q :
   P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
 Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 
-Lemma test_iFrame_later `{BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
+Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
 
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
@@ -555,7 +555,7 @@ Proof.
 Qed.
 
 Check "test_and_sep_affine_bi".
-Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   iIntros "[??]". iSplit; last done. Show. done.
 Qed.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index fda29fc12a90fc96d017e5eb99d1fab7343c74f1..0dbca72f4bf79e467472c44b99700f3542570f5c 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,9 +1,9 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   N : namespace
   P : iProp Σ
   ============================
@@ -15,9 +15,9 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   N : namespace
   P : iProp Σ
   ============================
@@ -31,9 +31,9 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   γ : gname
   p : Qp
   N : namespace
@@ -49,9 +49,9 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   γ : gname
   p : Qp
   N : namespace
@@ -68,14 +68,14 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   t : na_inv_pool_name
   N : namespace
   E1, E2 : coPset
   P : iProp Σ
-  H2 : ↑N ⊆ E2
+  H : ↑N ⊆ E2
   ============================
   _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
@@ -89,14 +89,14 @@
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
-  H0 : cinvG Σ
-  H1 : na_invG Σ
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
   t : na_inv_pool_name
   N : namespace
   E1, E2 : coPset
   P : iProp Σ
-  H2 : ↑N ⊆ E2
+  H : ↑N ⊆ E2
   ============================
   _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
@@ -132,12 +132,12 @@ Tactic failure: iInv: invariant "H2" not found.
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
+  invG0 : invG Σ
   I : biIndex
   N : namespace
   E : coPset
   𝓟 : iProp Σ
-  H0 : ↑N ⊆ E
+  H : ↑N ⊆ E
   ============================
   "HP" : ⎡ ▷ 𝓟 ⎤
   --------------------------------------∗
@@ -148,12 +148,12 @@ Tactic failure: iInv: invariant "H2" not found.
 1 subgoal
   
   Σ : gFunctors
-  H : invG Σ
+  invG0 : invG Σ
   I : biIndex
   N : namespace
   E : coPset
   𝓟 : iProp Σ
-  H0 : ↑N ⊆ E
+  H : ↑N ⊆ E
   ============================
   "HP" : ⎡ ▷ 𝓟 ⎤
   "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 545967539c3d03636ebe101eeb408c82afde3069..d369d746b6567fcb2c05a8e16b8108df65dffdb8 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -50,7 +50,7 @@ Section base_logic_tests.
 End base_logic_tests.
 
 Section iris_tests.
-  Context `{invG Σ, cinvG Σ, na_invG Σ}.
+  Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
   Lemma test_masks  N E P Q R :
@@ -223,7 +223,7 @@ Section iris_tests.
 End iris_tests.
 
 Section monpred_tests.
-  Context `{invG Σ}.
+  Context `{!invG Σ}.
   Context {I : biIndex}.
   Local Notation monPred := (monPred I (iPropI Σ)).
   Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 28cf7fdec5584dafc775e05be9faf266d4da18a4..f62241eabbdbca72445d95887cd66ee1f7f93545 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -266,7 +266,7 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
 Proof. by apply agree_eq. Qed.
 
 Section agree_map.
-  Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
+  Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}.
 
   Instance agree_map_ne : NonExpansive (agree_map f).
   Proof.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 7bfb354c4d0f3aaedbcc17d7425799bd02f710a0..d6f038dd57b91d7be8a1b34f9e0cc908b327ffc9 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -43,7 +43,7 @@ Definition auth_ofe_mixin : OfeMixin (auth A).
 Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
 Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
 
-Global Instance auth_cofe `{Cofe A} : Cofe authC.
+Global Instance auth_cofe `{!Cofe A} : Cofe authC.
 Proof.
   apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
     (λ x, (authoritative x, auth_own x))); by repeat intro.
@@ -113,7 +113,7 @@ Proof.
   destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
 Qed.
 
-Lemma auth_valid_discrete `{CmraDiscrete A} x :
+Lemma auth_valid_discrete `{!CmraDiscrete A} x :
   ✓ x ↔ match authoritative x with
         | Excl' a => auth_own x ≼ a ∧ ✓ a
         | None => ✓ auth_own x
@@ -125,12 +125,12 @@ Proof.
 Qed.
 Lemma auth_validN_2 n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
 Proof. by rewrite auth_validN_eq /= left_id. Qed.
-Lemma auth_valid_discrete_2 `{CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
 Proof. by rewrite auth_valid_discrete /= left_id. Qed.
 
 Lemma authoritative_valid  x : ✓ x → ✓ authoritative x.
 Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{CmraDiscrete A} x : ✓ x → ✓ auth_own x.
+Lemma auth_own_valid `{!CmraDiscrete A} x : ✓ x → ✓ auth_own x.
 Proof.
   rewrite auth_valid_discrete.
   destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 849a8ab8ea84129a09302cd5837a1e5b0df92645..41956b4412f33d5ea92dbfae4e75186eb47bf569 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -52,7 +52,7 @@ Proof.
 Qed.
 Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
 
-Global Instance excl_cofe `{Cofe A} : Cofe exclC.
+Global Instance excl_cofe `{!Cofe A} : Cofe exclC.
 Proof.
   apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
   - by intros n [a|] [b|]; split; inversion_clear 1; constructor.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 018ae86979bb83a8c9caa946c8b37823429273df..408e75386750355e0b6e31fdf95acc6cfd0851e8 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -353,7 +353,7 @@ Qed.
 
 Section freshness.
   Local Set Default Proof Using "Type*".
-  Context `{Infinite K}.
+  Context `{!Infinite K}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
     ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
   Proof.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 380c874b88be0a4abfd3d4e5264aefada85c0a2f..cdfbfdbd77f4de7fede17ac3774a1747839bc562 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -163,7 +163,7 @@ Section gset_disj.
 
   Section fresh_updates.
     Local Set Default Proof Using "Type*".
-    Context `{Infinite K}.
+    Context `{!Infinite K}.
 
     Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
       (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 5e57d9d16ebfd24e55188f9dc75465bb0bdabba7..8d9aa0db0086194ae2d81942f979aee5ee6e7948 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -58,12 +58,12 @@ Program Definition list_chain
     (c : chain listC) (x : A) (k : nat) : chain A :=
   {| chain_car n := default x (c n !! k) |}.
 Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
-Definition list_compl `{Cofe A} : Compl listC := λ c,
+Definition list_compl `{!Cofe A} : Compl listC := λ c,
   match c 0 with
   | [] => []
   | x :: _ => compl ∘ list_chain c x <$> seq 0 (length (c 0))
   end.
-Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
+Global Program Instance list_cofe `{!Cofe A} : Cofe listC :=
   {| compl := list_compl |}.
 Next Obligation.
   intros ? n c; rewrite /compl /list_compl.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 08ba333b2ef0f5385dc39ded303e70c2e291a8e8..9db6cf68316ea7e64f869080976387b5bb38bf1f 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -202,7 +202,7 @@ Lemma option_validI {A : cmraT} (mx : option A) :
 Proof. exact: uPred_primitive.option_validI. Qed.
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index d3ff12d81d6622b48e7e5a107fbfd1e62512dab8..aa2e11301236d328ee97c8216fa81e8a4bacf3b7 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -60,7 +60,7 @@ Proof.
 Qed.
 
 (** Timeless instances *)
-Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmraT} `{!CmraDiscrete A} (a : A) :
   Timeless (✓ a : uPred M)%I.
 Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
 Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 09e64079fc0000e6398afedb13fad4ec181eb674..c4a2fb3476f540dacc59cac710ba735a3c681d6f 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -16,7 +16,7 @@ Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
+  Context `{!invG Σ, !authG Σ A} {T : Type} (γ : gname).
 
   Definition auth_own (a : A) : iProp Σ :=
     own γ (◯ a).
@@ -60,7 +60,7 @@ Instance: Params (@auth_inv) 5 := {}.
 Instance: Params (@auth_ctx) 7 := {}.
 
 Section auth.
-  Context `{invG Σ, authG Σ A}.
+  Context `{!invG Σ, !authG Σ A}.
   Context {T : Type} `{!Inhabited T}.
   Context (f : T → A) (φ : T → iProp Σ).
   Implicit Types N : namespace.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 9e50462193999332963bb000f4e793d381f55833..881772bad59a179d067cf4ac48d5167e303cd3ee 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -17,7 +17,7 @@ Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
 Proof. solve_inG. Qed.
 
 Section box_defs.
-  Context `{invG Σ, boxG Σ} (N : namespace).
+  Context `{!invG Σ, !boxG Σ} (N : namespace).
 
   Definition slice_name := gname.
 
@@ -46,7 +46,7 @@ Instance: Params (@slice) 5 := {}.
 Instance: Params (@box) 5 := {}.
 
 Section box.
-Context `{invG Σ, boxG Σ} (N : namespace).
+Context `{!invG Σ, !boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 8239e7e3bb857b64b1388edc94f76d7c69362ecf..9d0ebd58040fed12ae0dd1772e18aeee60b966d0 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -12,7 +12,7 @@ Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{invG Σ, cinvG Σ}.
+  Context `{!invG Σ, !cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -23,7 +23,7 @@ End defs.
 Instance: Params (@cinv) 5 := {}.
 
 Section proofs.
-  Context `{invG Σ, cinvG Σ}.
+  Context `{!invG Σ, !cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 2277c86d09ba919f3d3bea035639ceb2177f5b67..0889c404dea27917a7a67c3585cee8af77f89d0b 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -7,14 +7,14 @@ Set Default Proof Using "Type".
 Export invG.
 Import uPred.
 
-Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
-Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
-Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
-Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
+Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. by eexists. Qed.
+Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
+Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
   uPred_fupd_aux.(seal_eq).
 
-Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
 Proof.
   split.
   - rewrite uPred_fupd_eq. solve_proper.
@@ -32,13 +32,13 @@ Proof.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
 Qed.
-Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
   {| bi_fupd_mixin := uPred_fupd_mixin |}.
 
-Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
 Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
 
-Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
+Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
 Proof.
   split.
   - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
@@ -59,8 +59,8 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
+Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}:
+  (∀ `{Hinv: !invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
 Proof.
   iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
   iPoseProof (Hfupd Hinv) as "H".
@@ -68,8 +68,8 @@ Proof.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma step_fupdN_soundness `{invPreG Σ} φ n :
-  (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
+Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
+  (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
   φ.
 Proof.
   intros Hiter.
@@ -86,8 +86,8 @@ Proof.
     iNext. by iMod "Hφ".
 Qed.
 
-Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
-  (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌝ : iProp Σ)%I)  →
+Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
+  (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌝ : iProp Σ)%I)  →
   φ.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index dfbaa78bf2de211c43b5f4e5c9bb0f7db9e1dcad..494844854ce1013d5d263b2b3b922a7b2d723df0 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -28,7 +28,7 @@ Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{hG : gen_heapG L V Σ}.
+  Context `{Countable L, hG : !gen_heapG L V Σ}.
 
   Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
     own (gen_heap_name hG) (● (to_gen_heap σ)).
@@ -72,7 +72,7 @@ Section to_gen_heap.
   Proof. by rewrite /to_gen_heap fmap_delete. Qed.
 End to_gen_heap.
 
-Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
@@ -81,7 +81,7 @@ Proof.
 Qed.
 
 Section gen_heap.
-  Context `{gen_heapG L V Σ}.
+  Context `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 4e0c9016ea3a6f381e11704bd087f13d60ac156a..cadd6f23126e056083bc2b25ef879546657e7eef 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
-Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I.
 Definition inv_aux : seal (@inv_def). by eexists. Qed.
 Definition inv {Σ i} := inv_aux.(unseal) Σ i.
@@ -16,7 +16,7 @@ Instance: Params (@inv) 3 := {}.
 Typeclasses Opaque inv.
 
 Section inv.
-Context `{invG Σ}.
+Context `{!invG Σ}.
 Implicit Types i : positive.
 Implicit Types N : namespace.
 Implicit Types P Q R : iProp Σ.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 41b81ed3301f59f216ecf773cb1b141291daf9d6..c92594bf03bd69529cc77263d2a513d64c3fe8ef 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -16,7 +16,7 @@ Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context `{invG Σ, na_invG Σ}.
+  Context `{!invG Σ, !na_invG Σ}.
 
   Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
     own p (CoPset E, GSet ∅).
@@ -30,7 +30,7 @@ Instance: Params (@na_inv) 3 := {}.
 Typeclasses Opaque na_own na_inv.
 
 Section proofs.
-  Context `{invG Σ, na_invG Σ}.
+  Context `{!invG Σ, !na_invG Σ}.
 
   Global Instance na_own_timeless p E : Timeless (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index e55af99d318d16718787b9d827ed3b7cb76bc4bf..7c6eebf436b4905547c176334cd5ef9760620e9c 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -47,11 +47,11 @@ Ltac solve_inG :=
   split; (assumption || by apply _).
 
 (** * Definition of the connective [own] *)
-Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
+Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
   ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
 Instance: Params (@iRes_singleton) 4 := {}.
 
-Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
+Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). by eexists. Qed.
 Definition own {Σ A i} := own_aux.(unseal) Σ A i.
@@ -61,7 +61,7 @@ Typeclasses Opaque own.
 
 (** * Properties about ghost ownership *)
 Section global.
-Context `{inG Σ A}.
+Context `{Hin: !inG Σ A}.
 Implicit Types a : A.
 
 (** ** Properties of [iRes_singleton] *)
@@ -113,9 +113,9 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
 Lemma later_own γ a : ▷ own γ a -∗ ◇ (∃ b, own γ b ∧ ▷ (a ≡ b)).
 Proof.
   rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
-  assert (NonExpansive (λ r : iResUR Σ, r (inG_id H) !! γ)).
+  assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
   { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
-  rewrite (f_equiv (λ r : iResUR Σ, r (inG_id H) !! γ) _ r).
+  rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
   rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
   rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
   { by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
@@ -125,7 +125,7 @@ Proof.
       cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
       by (by intros ?? ->).
     apply ownM_mono=> /=.
-    exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id H))) r).
+    exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
     intros i'. rewrite ofe_fun_lookup_op.
     destruct (decide (i' = inG_id _)) as [->|?].
     + rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
@@ -196,7 +196,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
+Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
 Proof.
   rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
   apply bupd_ownM_update, ofe_fun_singleton_update_empty.
@@ -206,13 +206,13 @@ Proof.
 Qed.
 
 (** Big op class instances *)
-Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
+Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} :
   WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
 Proof. split; try apply _. apply own_op. Qed.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{inG Σ A}.
+  Context `{!inG Σ A}.
   Implicit Types a b : A.
 
   Global Instance into_sep_own γ a b1 b2 :
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index bc0a581d9ccc9d3c7d93fc9cfd8f401c24c371cc..fc0710c9c14509985d83aa77f0c1cf0d22161262 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -17,14 +17,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
   subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
-Definition saved_anything_own `{savedAnythingG Σ F}
+Definition saved_anything_own `{!savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
-  Context `{savedAnythingG Σ F}.
+  Context `{!savedAnythingG Σ F}.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
@@ -65,22 +65,22 @@ End saved_anything.
 Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
 Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
 
-Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
   saved_anything_own (F := ▶ ∙) γ (Next P).
 
-Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
   Contractive (saved_prop_own γ).
 Proof. solve_contractive. Qed.
 
-Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+Lemma saved_prop_alloc_strong `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
+Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
   (|==> ∃ γ, saved_prop_own γ P)%I.
 Proof. iApply saved_anything_alloc. Qed.
 
-Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
+Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
   saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
 Proof.
   iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
@@ -90,25 +90,25 @@ Qed.
 Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
 
-Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
   saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
 
-Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
+Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
   Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
 Proof.
   solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
 Qed.
 
-Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :
   (|==> ∃ γ, saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc. Qed.
 
 (* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
   saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
 Proof.
   unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 368cb41ed00c050203e744997c4e141b0a388006..6004e1b4bb4d4d54fd25f42b6d862a2e57364da8 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts :
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{stsG Σ sts} (γ : gname).
+  Context `{!stsG Σ sts} (γ : gname).
 
   Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
     own γ (sts_frag S T).
@@ -57,7 +57,7 @@ Instance: Params (@sts_own) 5 := {}.
 Instance: Params (@sts_ctx) 6 := {}.
 
 Section sts.
-  Context `{invG Σ, stsG Σ sts}.
+  Context `{!invG Σ, !stsG Σ sts}.
   Implicit Types φ : sts.state sts → iProp Σ.
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Σ.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 7443ddc9bf302aac73bb1afcc8052bc56d3bad66..a727317d2af5ab0bf82a69e1de6e9e6da7c9cc8f 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -∗ |={E1,E2}=> Q))%I.
 Arguments vs {_ _} _ _ _%I _%I.
 
@@ -22,7 +22,7 @@ Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
    format "P  ={ E }=>  Q") : stdpp_scope.
 
 Section vs.
-Context `{invG Σ}.
+Context `{!invG Σ}.
 Implicit Types P Q R : iProp Σ.
 Implicit Types N : namespace.
 
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index cf629405a33d3d70225970f81ff57c69701cf97a..78cb9f7645341533b0ad7ffe520e31e651fbdbdf 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -35,30 +35,30 @@ Import invG.
 
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
-Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
 Instance: Params (@invariant_unfold) 1 := {}.
 Instance: Params (@ownI) 3 := {}.
 
-Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
 Instance: Params (@ownE) 3 := {}.
 
-Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
 Instance: Params (@ownD) 3 := {}.
 
-Definition wsat `{invG Σ} : iProp Σ :=
+Definition wsat `{!invG Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
     own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
-Context `{invG Σ}.
+Context `{!invG Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
@@ -194,7 +194,7 @@ Qed.
 End wsat.
 
 (* Allocation of an initial world *)
-Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
+Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
   iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 6caa4627b3f435395fb0917bf1295258aff8c3db..9475d6c5aac49fa78556477d53ab40b99d86213c 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -8,7 +8,7 @@ Section class_instances.
 Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
 
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
   @IntoPure (uPredI M) (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 1e14ffb24f22636529acd8094c703c86076742c1..f6052c634c3bf2af8d0d23e21874199c7ff465f4 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -693,7 +693,7 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
   NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
 Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
 
-Lemma fun_ext `{B : A → ofeT} (g1 g2 : ofe_fun B) :
+Lemma fun_ext {A} {B : A → ofeT} (g1 g2 : ofe_fun B) :
   (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
 Proof. by unseal. Qed.
 Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) :
@@ -797,7 +797,7 @@ Proof. unseal. by destruct mx. Qed.
 Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 02301b8fb6d4d5a73dad9472e2f9234066a6b51d..4bfe13696527a5e87670f013ab3c82653688398b 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -14,8 +14,8 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
-  (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
+Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
+  (∀ `{!heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index c44b33126bb8dda9b838146fe83724b1ee2c344a..d1d6513d3a7391c260f8fa986e0f7c5e318d7042 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -9,7 +9,7 @@ Definition assert : val :=
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
-Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
   WP assert (LamV BAnon e)%V @ E [{ Φ }].
 Proof.
@@ -17,7 +17,7 @@ Proof.
   wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
 
-Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
   WP assert (LamV BAnon e)%V @ E {{ Φ }}.
 Proof.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 453b67420f487170d20de0153809aa6319fe9b68..17571589b3cf5e034b0c2b06220129298fdbe03e 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
   heapG_proph_mapG :> proph_mapG proph_id val Σ
 }.
 
-Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
+Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp σ κs _ :=
     (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
@@ -117,7 +117,7 @@ Instance pure_injrc (v : val) :
   PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
 Proof. solve_pure_exec. Qed.
 
-Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
+Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
   PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
 Proof. unfold AsRecV in *. solve_pure_exec. Qed.
 
@@ -152,7 +152,7 @@ Instance pure_case_inr v e1 e2 :
 Proof. solve_pure_exec. Qed.
 
 Section lifting.
-Context `{heapG Σ}.
+Context `{!heapG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index fe772614870bd10ba047cc70ff152c0d24e4094c..2f718e7f658a813ad30fba0625839990ac3cddd5 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -7,11 +7,11 @@ From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
-Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
   (∀ (e'':=e'), e = e'') →
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
@@ -28,7 +28,7 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
 
-Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
@@ -47,10 +47,10 @@ Proof.
   rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
+Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
+Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 
@@ -135,12 +135,12 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
 Tactic Notation "wp_pair" := wp_pure (Pair _ _).
 Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
 
-Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
+Lemma tac_wp_bind `{!heapG Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
-Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
+Lemma tac_twp_bind `{!heapG Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
   envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
@@ -171,7 +171,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
 
 (** Heap tactics *)
 Section heap.
-Context `{heapG Σ}.
+Context `{!heapG Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 39308f1a99d1832dd0c631e08a1563466d588af9..4e965dd67cff9f4b82bd172d3955447573f76b81 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -31,7 +31,7 @@ Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context `{pG : proph_mapG P V Σ}.
+  Context `{Countable P, pG : !proph_mapG P V Σ}.
 
   (** The first resolve for [p] in [pvs] *)
   Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
@@ -127,7 +127,7 @@ Section to_proph_map.
 End to_proph_map.
 
 
-Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
+Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
 Proof.
   iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
@@ -137,7 +137,7 @@ Proof.
 Qed.
 
 Section proph_map.
-  Context `{proph_mapG P V Σ}.
+  Context `{Countable P, !proph_mapG P V Σ}.
   Implicit Types p : P.
   Implicit Types v : option V.
   Implicit Types R : proph_map P V.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 8cfbfb39bd1d49f491d4d3909e6b21c29efffc7c..df83c1542262baae6879521cf1110864640ee607 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -4,8 +4,8 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition heap_total Σ `{heapPreG Σ} s e σ φ :
-  (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
+Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
+  (∀ `{!heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
   sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 770e56fb1b01dbd4ef41864d71a7d772e5174947..6bca02624e699d13b35fdcfa79b8bf446d16f536 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -33,7 +33,7 @@ Proof.
 Qed.
 
 Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -173,8 +173,8 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
-  (∀ `{Hinv : invG Σ} κs,
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
+  (∀ `{Hinv : !invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -198,8 +198,8 @@ Proof.
     iApply (@wptp_safe _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
 Qed.
 
-Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
-  (∀ `{Hinv : invG Σ} κs,
+Theorem wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
+  (∀ `{Hinv : !invG Σ} κs,
      (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
@@ -212,8 +212,8 @@ Proof.
   iIntros "_". by iApply fupd_mask_weaken.
 Qed.
 
-Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
-  (∀ `{Hinv : invG Σ} κs,
+Theorem wp_strong_all_adequacy Σ Λ `{!invPreG Σ} s e σ1 v vs σ2 φ :
+  (∀ `{Hinv : !invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -232,8 +232,8 @@ Proof.
     with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
-  (∀ `{Hinv : invG Σ} κs κs',
+Theorem wp_invariance Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
+  (∀ `{Hinv : !invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -253,8 +253,8 @@ Qed.
 
 (* An equivalent version that does not require finding [fupd_intro_mask'], but
 can be confusing to use. *)
-Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
-  (∀ `{Hinv : invG Σ} κs κs',
+Corollary wp_invariance' Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
+  (∀ `{Hinv : !invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 25df772be33d0ef798f62fb779f4a33050d1a96c..487acd3567c327b27d4fdaf44c1799c56f605a39 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
 example where we want it to be anything else. *)
-Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
+Definition atomic_wp `{!irisG Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
   (Eo : coPset) (* (outer) mask *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
@@ -94,7 +94,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
 
 (** Theory *)
 Section lemmas.
-  Context `{irisG Λ Σ} {TA TB : tele}.
+  Context `{!irisG Λ Σ} {TA TB : tele}.
   Notation iProp := (iProp Σ).
   Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
 
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 68b183168668cd92099dae4a8812588c743fed6a..dd0fff9916907272b5ec725d8065efec28b11b1c 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -201,7 +201,7 @@ Section ectx_language.
   Qed.
 
   (* Every evaluation context is a context. *)
-  Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
+  Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K).
   Proof.
     split; simpl.
     - eauto using fill_not_val.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 12c6d3f0e2da712a3f32dfbe382655c45d915728..a164cb131c7094b1577c1284b296eab7c60ad42f 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section wp.
-Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 603d216516f1f8c2bb60ae876a68106f656f33f7..c23bfbef329e4a621c812c7205624ea7e7da7491 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -137,8 +137,8 @@ Section ectxi_language.
     intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
   Qed.
 
-  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
-  Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
+  Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki).
+  Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
 End ectxi_language.
 
 Arguments fill {_} _ _%E.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index b6587a44182756f9de2ffe75332f66f89fe29ccf..ff46550fc76bb30a4302f841d4ec3316eccbf985 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
+Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
   (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
 Instance: Params (@ht) 5 := {}.
@@ -41,7 +41,7 @@ Notation "{{ P } } e ? {{ v , Q } }" := (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
    format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
 
 Section hoare.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val Λ → iProp Σ.
@@ -89,7 +89,7 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
+Lemma ht_bind `{!LanguageCtx Λ K} s E P Φ Φ' e :
   {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
   ⊢ {{ P }} K e @ s; E {{ Φ' }}.
 Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 378d68c79722d1361129a8023e92558121863785..483d9a244017fde0f647d2d079741c7ce7e7ce98 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,8 +53,9 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
     to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
     ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
 }.
+Arguments LanguageCtx : clear implicits.
 
-Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
+Instance language_ctx_id Λ : LanguageCtx Λ (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
 Inductive atomicity := StronglyAtomic | WeaklyAtomic.
@@ -141,19 +142,19 @@ Section language.
     Atomic StronglyAtomic e → Atomic a e.
   Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
 
-  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
+  Lemma reducible_fill `{!LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
     intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
-  Lemma reducible_no_obs_fill `{LanguageCtx Λ K} e σ :
+  Lemma reducible_no_obs_fill `{!LanguageCtx Λ K} e σ :
     to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
   Proof.
     intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
-  Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
+  Lemma irreducible_fill `{!LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
@@ -185,7 +186,7 @@ Section language.
   Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
     pure_exec : φ → relations.nsteps pure_step n e1 e2.
 
-  Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
+  Lemma pure_step_ctx K `{!LanguageCtx Λ K} e1 e2 :
     pure_step e1 e2 →
     pure_step (K e1) (K e2).
   Proof.
@@ -197,13 +198,13 @@ Section language.
       + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 
-  Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
+  Lemma pure_step_nsteps_ctx K `{!LanguageCtx Λ K} n e1 e2 :
     relations.nsteps pure_step n e1 e2 →
     relations.nsteps pure_step n (K e1) (K e2).
   Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
 
   (* We do not make this an instance because it is awfully general. *)
-  Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
+  Lemma pure_exec_ctx K `{!LanguageCtx Λ K} φ n e1 e2 :
     PureExec φ n e1 e2 →
     PureExec φ n (K e1) (K e2).
   Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 4d9e79a9dcb7a140dad8ee137686d341d5224fbc..3219b14562eebf13e43e3b30f9b20a44c8b43230 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section lifting.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
@@ -53,7 +53,7 @@ Proof.
   iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
 Qed.
 
-Lemma wp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E E' Φ e1 :
+Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
   (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
@@ -70,7 +70,7 @@ Proof.
   iDestruct ("H" with "[//]") as "H". simpl. iFrame.
 Qed.
 
-Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
+Lemma wp_lift_pure_stuck `{!Inhabited (state Λ)} E Φ e :
   (∀ σ, stuck e σ) →
   True ⊢ WP e @ E ?{{ Φ }}.
 Proof.
@@ -120,7 +120,7 @@ Proof.
   by iApply "H".
 Qed.
 
-Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
     κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
@@ -132,7 +132,7 @@ Proof.
   iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
 Qed.
 
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
+Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
@@ -145,7 +145,7 @@ Proof.
   - by iApply (step_fupd_wand with "Hwp").
 Qed.
 
-Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+Lemma wp_pure_step_later `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   ▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 17530e77ec0fe2a4721d7177c33c80c7bbc361c8..d48ef7a93774f68dca2d6fb5f41f21336ee290a5 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -20,7 +20,7 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
   ownP_name : gname;
 }.
 
-Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := {
+Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
   iris_invG := ownP_invG;
   state_interp σ κs _ := own ownP_name (● (Excl' σ))%I;
   fork_post _ := True%I;
@@ -40,15 +40,15 @@ Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
 Proof. solve_inG. Qed.
 
 (** Ownership *)
-Definition ownP `{ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
+Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
   own ownP_name (◯ (Excl' σ)).
 
 Typeclasses Opaque ownP.
 Instance: Params (@ownP) 3 := {}.
 
 (* Adequacy *)
-Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
-  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
+  (∀ `{!ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
@@ -59,8 +59,8 @@ Proof.
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
 Qed.
 
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
-  (∀ `{ownPG Λ Σ},
+Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
+  (∀ `{!ownPG Λ Σ},
       ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
       |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc erased_step ([e], σ1) (t2, σ2) →
@@ -81,7 +81,7 @@ Qed.
 
 (** Lifting *)
 Section lifting.
-  Context `{ownPG Λ Σ}.
+  Context `{!ownPG Λ Σ}.
   Implicit Types s : stuckness.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
@@ -134,7 +134,7 @@ Section lifting.
       by iDestruct (ownP_eq with "Hσ Hσf") as %->.
   Qed.
 
-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
+  Lemma ownP_lift_pure_step `{!Inhabited (state Λ)} s E Φ e1 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1) →
     (▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
@@ -193,7 +193,7 @@ Section lifting.
     iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
   Qed.
 
-  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
@@ -204,7 +204,7 @@ End lifting.
 
 Section ectx_lifting.
   Import ectx_language.
-  Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
+  Context {Λ : ectxLanguage} `{!ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
   Implicit Types s : stuckness.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index b6243370d78081ed8aa584f9b67f0d0606331758..9e8ba8f6dbfe6f2be17f8b305b95d6167248ebe3 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
@@ -114,8 +114,8 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
-  (∀ `{Hinv : invG Σ},
+Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
+  (∀ `{Hinv : !invG Σ},
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 7a3e8e977bdb9a6384ed4d5ff10e269a291b7db1..3e1168bfcc0d6b725e691b603856dfd91e195fd0 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section wp.
-Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index fe953845e0a835ef41b70f30de213dba9fb8c78f..c2e7a9086c0da1dd55d196e791c494c20c41a5e6 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section lifting.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
@@ -26,7 +26,7 @@ Lemma twp_lift_step s E Φ e1 :
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
 (** Derived lifting lemmas. *)
-Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
+Lemma twp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E Φ e1 :
   (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
   (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }])
@@ -65,7 +65,7 @@ Proof.
   iApply twp_value; last done. by apply of_to_val.
 Qed.
 
-Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+Lemma twp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
   (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
     κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
@@ -76,7 +76,7 @@ Proof.
   iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
 Qed.
 
-Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+Lemma twp_pure_step `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index e3da620ff1bbb625249f07a2de1dcb7432f3b8e4..24173b69128f471c3da9ce39c880f3da29f5e134 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fixpoint big_op.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition twp_pre `{irisG Λ Σ} (s : stuckness)
+Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
       (wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
@@ -19,7 +19,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
          [∗ list] ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
-Lemma twp_pre_mono `{irisG Λ Σ} s
+Lemma twp_pre_mono `{!irisG Λ Σ} s
     (wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
   ((□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
   ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ)%I.
@@ -36,12 +36,12 @@ Proof.
 Qed.
 
 (* Uncurry [twp_pre] and equip its type with an OFE structure *)
-Definition twp_pre' `{irisG Λ Σ} (s : stuckness) :
+Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
   (prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ) →
   prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ :=
     curry3 ∘ twp_pre s ∘ uncurry3.
 
-Local Instance twp_pre_mono' `{irisG Λ Σ} s : BiMonoPred (twp_pre' s).
+Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
   - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
@@ -51,15 +51,15 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
+Definition twp_def `{!irisG Λ Σ} (s : stuckness) (E : coPset)
     (e : expr Λ) (Φ : val Λ → iProp Σ) :
   iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux `{irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
-Instance twp' `{irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
-Definition twp_eq `{irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
+Definition twp_aux `{!irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
+Instance twp' `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
+Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
 
 Section twp.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -147,7 +147,7 @@ Proof.
     iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
 Qed.
 
-Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
+Lemma twp_bind K `{!LanguageCtx Λ K} s E e Φ :
   WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] -∗ WP K e @ s; E [{ Φ }].
 Proof.
   revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
@@ -169,7 +169,7 @@ Proof.
   - by setoid_rewrite and_elim_r.
 Qed.
 
-Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
+Lemma twp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
   WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
 Proof.
   iIntros "H". remember (K e) as e' eqn:He'.
@@ -251,7 +251,7 @@ End twp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{irisG Λ Σ}.
+  Context `{!irisG Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 65513253b663208b17b632dbc092cc29273903ad..47ba39abeb9d890e76dfdebbb99616bb33706335 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -22,7 +22,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
 }.
 Global Opaque iris_invG.
 
-Definition wp_pre `{irisG Λ Σ} (s : stuckness)
+Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
   match to_val e1 with
@@ -36,20 +36,20 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
-Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
+Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} (s : stuckness) :
+Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
-Instance wp' `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
-Definition wp_eq `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
+Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
+Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
+Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
 
 Section wp.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
 Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
@@ -143,7 +143,7 @@ Proof.
   iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
+Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ :
   WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
@@ -160,7 +160,7 @@ Proof.
   iModIntro. iFrame "Hσ Hefs". by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
   WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
@@ -252,7 +252,7 @@ End wp.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{irisG Λ Σ}.
+  Context `{!irisG Λ Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.