From e823cff642c092c58d869df0e859c5efe231eae0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Feb 2019 17:44:14 +0100
Subject: [PATCH] Comment about `Set_`.

---
 theories/base.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index a3e01836..e0034cc2 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 ∉ ∅;
-- 
GitLab