From 6823251d47a7b9c7d90ed047b4b27288f2ff9204 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 10 Nov 2021 12:08:43 -0500
Subject: [PATCH] remove an outdated comment

---
 iris/algebra/gmap.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 3ea2bba6f..7a7c56546 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -94,7 +94,6 @@ Lemma insert_idN n m i x :
   m !! i â‰¡{n}â‰¡ Some x â†’ <[i:=x]>m â‰¡{n}â‰¡ m.
 Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
 
-(** Internalized properties *)
 End ofe.
 
 Global Instance map_seq_ne {A : ofe} start :
-- 
GitLab