diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 65375c186666ecc2b3813a828b6a634f2c7cfac0..ea19cf82af00a0507f3083c814050663cb65fbd0 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -29,7 +29,7 @@ Section proof.
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
 
-  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
+  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
 
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.