Remove namespaces from lock API.

theories/heap_lang/lib/lock.v

@@ -10,31 +10,31 @@ Structure lock Σ `{!heapG Σ} := Lock {
   (* -- predicates -- *)
   (* name is used to associate locked with is_lock *)
   name : Type;
-  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
+  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;
+  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 }}}
+  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 _.

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.

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,