From 047d1fa5b95debd96dfe2c00e216186872af1048 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Fri, 17 Dec 2021 11:16:07 +0000
Subject: [PATCH] coqdocify

---
 iris/algebra/lib/dfrac_agree.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/lib/dfrac_agree.v b/iris/algebra/lib/dfrac_agree.v
index 388fd6dbc..693287c55 100644
--- a/iris/algebra/lib/dfrac_agree.v
+++ b/iris/algebra/lib/dfrac_agree.v
@@ -126,4 +126,4 @@ Section lemmas.
 End lemmas.
 
 Typeclasses Opaque to_dfrac_agree.
-(* to_frac_agree is deliberately transparent to reuse the to_dfrac_agree instances *)
+(* [to_frac_agree] is deliberately transparent to reuse the [to_dfrac_agree] instances *)
-- 
GitLab