diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index b76206de240513eb8585779ff276583a99cdab37..6fdc67828687d48a4192416d8061caa820dda72e 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -271,7 +271,7 @@ candidate for [P], but not [R], or the other way around.
 
 Note that [FromSep] and [CombineSepAs] have nearly the same definition. However,
 they have different Hint Modes and are used for different tactics. [FromSep] is
-used to compute the two new goals obtained after applying `iSplitL`/`iSplitR`,
+used to compute the two new goals obtained after applying [iSplitL]/[iSplitR],
 taking the current goal as input. [CombineSepAs] is used to combine two
 hypotheses into one. *)
 Class CombineSepAs {PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.