diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 5e5ad25edc624b67d558a9a201034a0a16d3d68d..f9059566e4b4ded7c276d72aac613f4ece56f56a 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -31,7 +31,7 @@ Context `{!heapG Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
-                   ∃ v, ⌜lv = SOMEV v⌝ ∗ (Ψ v ∨ own γ (Excl ()))))%I.
+                   ∃ w, ⌜lv = SOMEV w⌝ ∗ (Ψ w ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 9da9bb33f18ab4a625e29d50eb145b0a82a882e1..23b63251c0c89912fd501d080765eb22d5000196 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -36,7 +36,7 @@ Section proof.
 
   Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
+  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
   Proof. solve_proper. Qed.
 
   (** The main proofs. *)
@@ -90,6 +90,6 @@ End proof.
 
 Typeclasses Opaque is_lock locked.
 
-Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 7a9f78cd88906256508fae367b401f36579d7ee1..7437f74833d1af6324e16db7e7080036bf757e16 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -166,6 +166,6 @@ End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.