diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 52e10620358daa91fa14b5b64f42110d90f56414..4ab5fe0a8fab9a3749ccdcdf11d0a7ea38ec79a5 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -68,8 +68,8 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :: lockG Σ;
-  chanG_protoG :: protoG Σ val;
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
 }.
 Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index b5674883171d4e9738fa22a3f5fedc976e1fe6ac..c0d9a33e63b7977a788b56e7d47d10de7a2626c2 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -129,7 +129,7 @@ Section example.
        "v2")
     ).
 
-  Lemma lock_example_spec jcc rcc c (x1 y1 : Z) :
+  Lemma lock_example_spec `{!lockG Σ} jcc rcc c (x1 y1 : Z) :
     {{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
       lock_example #jcc #rcc c
     {{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index fb9a56d4dcc89f8a098a20347f3c0dea718416de..b512bc099a5743ada8f94abb1ad7ac3c467a1907 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -35,7 +35,7 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition prog_prot : iProto Σ :=
@@ -119,7 +119,7 @@ Section double.
 End double.
 
 Section double_fc.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
   Definition prog_prot_fc (P : val → val → iProp Σ) : iProto Σ :=