diff --git a/tests/lock.v b/tests/lock.v
index 15f7337410043fe56dcc81d5e5e469979f0177bd..fda5baa55890a681dbf4e400da5b0927041e4024 100644
--- a/tests/lock.v
+++ b/tests/lock.v
@@ -46,8 +46,8 @@ Section lock_spin.
     ⊢ WP lock_client_spin {{ _, True }}.
   Proof.
     unfold lock_client_spin.
-   (* This should not unfold the `newlock`, `acquire`, and `release`
-    projections. That is, it should not show `spin_lock.<something>`. *)
+    (* This should not unfold the [newlock], [acquire], and [release]
+    projections. That is, it should not show [spin_lock.<something>]. *)
     simpl. Show.
     wp_alloc l as "Hl".
     wp_smart_apply (newlock_spec (∃ n : Z, l ↦ #n) with "[Hl]")