From 9f19f1ab81c78ed04113fd65188e5781cc4632e6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 12 Mar 2020 23:17:09 +0100
Subject: [PATCH] Fix typo.

---
 theories/algebra/ofe.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index ad309364b..af1b04545 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -887,7 +887,7 @@ End discrete_ofe.
 Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
 (** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
 find another one, like [ofe_equivalence], in the case of aliases. See also
-https://gitlab.mpi-sws.org/iris/iris/issues/229 *)
+https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
 Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL eq_equivalence)).
 
 (** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
-- 
GitLab