From 45e5a05207d1919b16494d4be6b90cd9130d5f15 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Mar 2023 09:47:45 +0100
Subject: [PATCH] Coqdoc.

---
 iris/proofmode/classes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index b76206de2..6fdc67828 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.
-- 
GitLab