diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6e00c253c7298f275699d8b5c9275b5c1703f5d7..f3bd2388a2e1ddd69c6ce2713ce67819110b6313 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -94,6 +94,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Affine, absorbing, persistent and timeless instances for telescopes.
 * Better support for telescopes in the proof mode, i.e., all tactics should
   recognize and distribute telescopes now.
+* Remove namespace `N` from `is_lock`.
 
 **Changes in heap_lang:**
 
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 184b62fd4b524fff8033ef918d05b9b7137c4996..77f57e59b7a2dd437c9dabbeec77213750ad8cbb 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -3,38 +3,40 @@ From iris.heap_lang Require Export lifting notation.
 Set Default Proof Using "Type".
 
 Structure lock Σ `{!heapG Σ} := Lock {
-  (* -- operations -- *)
+  (** * Operations *)
   newlock : val;
   acquire : val;
   release : val;
-  (* -- predicates -- *)
-  (* name is used to associate locked with is_lock *)
+  (** * Predicates *)
+  (** [name] is used to associate locked with [is_lock] *)
   name : Type;
-  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
+  (** No namespace [N] parameter because we only expose program specs, which
+  anyway have the full mask. *)
+  is_lock (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked (γ: name) : iProp Σ;
-  (* -- general properties -- *)
-  is_lock_ne N γ lk : Contractive (is_lock N γ lk);
-  is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
-  is_lock_iff N γ lk R1 R2 :
-    is_lock N γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock N γ lk R2;
+  (** * General properties of the predicates *)
+  is_lock_ne γ lk : Contractive (is_lock γ lk);
+  is_lock_persistent γ lk R : Persistent (is_lock γ lk R);
+  is_lock_iff γ lk R1 R2 :
+    is_lock γ lk R1 -∗ ▷ □ (R1 ↔ R2) -∗ is_lock γ lk R2;
   locked_timeless γ : Timeless (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
-  (* -- operation specs -- *)
-  newlock_spec N (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
-  acquire_spec N γ lk R :
-    {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
-  release_spec N γ lk R :
-    {{{ is_lock N γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
+  (** * Program specs *)
+  newlock_spec (R : iProp Σ) :
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}};
+  acquire_spec γ lk R :
+    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
+  release_spec γ lk R :
+    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
 
 Arguments newlock {_ _} _.
 Arguments acquire {_ _} _.
 Arguments release {_ _} _.
-Arguments is_lock {_ _} _ _ _ _ _.
+Arguments is_lock {_ _} _ _ _ _.
 Arguments locked {_ _} _ _.
 
 Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
-  Proper ((≡) ==> (≡)) (is_lock L N γ lk) := ne_proper _.
+Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
+  Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index d9be8c585c60044a9b962465a22be0df15ec8453..d56b2ae6225d8a00d8108250589a5a41a9d11d3c 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -21,7 +21,8 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+  Context `{!heapG Σ, !lockG Σ}.
+  Let N := nroot .@ "spin_lock".
 
   Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 93b60961cb81a53bdeded9d0b0f49c7a058dc1ad..c6ce4c057d725059d083ebd6812f59680dbf6a9f 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -37,7 +37,8 @@ Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapG Σ, !tlockG Σ} (N : namespace).
+  Context `{!heapG Σ, !tlockG Σ}.
+  Let N := nroot .@ "ticket_lock".
 
   Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
     (∃ o n : nat,