diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 3ea2bba6f2b23880a3dca1e11fb013ea6950e34d..7a7c56546aab3c285539a3aa05ba72d6122560b5 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 :