diff --git a/opam b/opam
index cd4fd5ede5bf0f0fa49413b519f4a621b3a27ea4..8358c2bf824a048f26c113b569d1c8d06027b70e 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-04-02.4.739cc004") | (= "dev") }
+  "coq-iris" { (= "dev.2020-04-04.2.c2367a65") | (= "dev") }
 ]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 4b7295c91cc69ad0f26951580d7b5b48ec2455e8..e495bd19ebea3996dfb1a8822523f35220129768 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -61,8 +61,6 @@ Definition recv : val :=
     end.
 
 (** * Setup of Iris's cameras *)
-Definition chanN := nroot .@ "chan".
-
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
   chanG_protoG :> protoG Σ val;
@@ -92,7 +90,7 @@ Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
   ∃ γ s (l r : loc) (lk : val),
     ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
-    is_lock chanN (chan_lock_name γ) lk (∃ vsl vsr,
+    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
       llist sbi_internal_eq l vsl ∗
       llist sbi_internal_eq r vsr ∗
       iProto_ctx (chan_proto_name γ) vsl vsr) ∗
@@ -199,7 +197,7 @@ Section channel.
     wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
     wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
     iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
-    wp_apply (newlock_spec chanN (∃ vsl vsr,
+    wp_apply (newlock_spec (∃ vsl vsr,
       llist sbi_internal_eq l vsl ∗ llist sbi_internal_eq r vsr ∗
       iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame. }
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 08b0cf02c4a96fbbbb6de7f590339fb5fdf724dd..2ad65fe5110892341bfa6a735a146a70435cc23a 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -281,7 +281,7 @@ Proof.
   - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
-    wp_apply (newlock_spec nroot (∃ n, server γ n ε ∗
+    wp_apply (newlock_spec (∃ n, server γ n ε ∗
       c ↣ iProto_dual (prot_lock n))%I
       with "[Hc Hs]"); first by eauto with iFrame.
     iIntros (lk γlk) "#Hlk".
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 5a94125636cfd43d5fa10bb8a3da6cb5bc95871f..42ca8c1aabb27021c2b37cf16909fa9ea21d4485 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -90,7 +90,7 @@ Section map.
 
   Lemma par_map_worker_spec γl γ vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
+    {{{ is_lock γl lk (map_worker_lock_inv γ c) ∗ client γ (∅ : gmultiset A) }}}
       par_map_worker vmap lk c
     {{{ RET #(); True }}}.
   Proof.
@@ -130,7 +130,7 @@ Section map.
 
   Lemma par_map_workers_spec γl γ n vmap lk c :
     map_spec vmap -∗
-    {{{ is_lock nroot γl lk (map_worker_lock_inv γ c) ∗
+    {{{ is_lock γl lk (map_worker_lock_inv γ c) ∗
         [∗] replicate n (client γ (∅:gmultiset A)) }}}
       par_map_workers #n vmap lk c
     {{{ RET #(); True }}}.
@@ -153,7 +153,7 @@ Section map.
   Proof.
     iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
-    wp_apply (newlock_spec nroot (map_worker_lock_inv γ c) with "[Hc Hs]").
+    wp_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
     { iExists n, ∅. iFrame. }
     iIntros (lk γl) "#Hlk".
     wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.