diff --git a/tests/proofmode.v b/tests/proofmode.v
index d5782bd97be10f7e771e4ccf328eb474b35593c9..e1c4ad8130edbb6d8f0ca792cb4b73ff0cf7d483 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -127,8 +127,8 @@ Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
 Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
 Proof. by iIntros (x). Qed.
 
-(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
-`False` and performs false elimination. *)
+(** Prior to 0b84351c this used to loop, now [iAssumption] instantiates [R] with
+[False] and performs false elimination. *)
 Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
 Proof. eexists. iIntros "?" (P). iAssumption. Qed.