Don't leak that locks are used internally in channels.

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 Σ.

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;

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 Σ :=