diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index ecca3cff5f55b3ee3f2b05612de492be4c852541..7f7ffb78bdcc076b8d9a6f484687a44094829de4 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.