From af52dfd83d88727593188fd2bf67404ae3f8f7e5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 30 Aug 2023 09:51:36 +0000
Subject: [PATCH] coqdoc

---
 tests/lock.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/lock.v b/tests/lock.v
index 15f733741..fda5baa55 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]")
-- 
GitLab