diff --git a/theories/base.v b/theories/base.v
index a3e0183609e5f30cf850477feac4c8674af2b346..e0034cc2e96d56e1359eeed9b65ed19151e7831e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1114,7 +1114,10 @@ Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 (** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
 elements of type [A]. The first class, [SemiSet] does not include intersection
 and difference. It is useful for the case of lists, where decidable equality
-is needed to implement intersection and difference, but not union. *)
+is needed to implement intersection and difference, but not union.
+
+Note that we cannot use the name [Set] since that is a reserved keyword. Hence
+we use [Set_]. *)
 Class SemiSet A C `{ElemOf A C,
     Empty C, Singleton A C, Union C} : Prop := {
   not_elem_of_empty (x : A) : x ∉ ∅;