From c4b14c5885086d6dc8ee54f35a86ee088bbb0a65 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:34:23 +0100
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

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

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index ecca3cff..7f7ffb78 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -350,7 +350,7 @@ Section map.
   Lemma set_map_union (f : A → B) (X Y : C) :
     set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y.
   Proof. set_solver. Qed.
-  (** This cannot be using [=] because list_to_set_singleton does not hold for [=]. *)
+  (** This cannot be using [=] because [list_to_set_singleton] does not hold for [=]. *)
   Lemma set_map_singleton (f : A → B) (x : A) :
     set_map (C:=C) (D:=D) f {[x]} ≡ {[f x]}.
   Proof. set_solver. Qed.
-- 
GitLab