From 0b853e2a60bd1fe5f9abc19afff982ebcc733fde Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2022 09:09:37 +0200
Subject: [PATCH] Coqdoc.

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

diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index ab4a3c03b..a0d8f1342 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -20,7 +20,7 @@ particular, [MakeX] instances should not have [Affine] or [Absorbing] premises
 (because these could invoke a recursive search). Instances for [MakeX] instances
 typically look only at the top-level symbol of the input, or check if the whole
 BI is affine (via the [BiAffine] class) -- the latter can be linear in
-the size of `PROP` itself, but is still independent of the size of the term.
+the size of [PROP] itself, but is still independent of the size of the term.
 
 One could imagine a smarter way of "cleaning up", as implemented in
 https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/450 for some modalities,
-- 
GitLab