From 012f94214c7d7678d3dc6c3b1b91ac5890c3c90e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Apr 2023 11:52:44 +0200
Subject: [PATCH] Coqdoc.

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

diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 353b262a7..1242c5314 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -1,7 +1,7 @@
 (** Ghost state for a monotonically increasing nat, wrapping the [mono_natR]
 RA. Provides an authoritative proposition [mono_nat_auth_own γ q n] for the
 underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
-witnessing that the authoritative nat is at least m.
+witnessing that the authoritative nat is at least [m].
 
 The key rules are [mono_nat_lb_own_valid], which asserts that an auth at [n] and
 a lower-bound at [m] imply that [m ≤ n], and [mono_nat_update], which allows to
-- 
GitLab