diff --git a/util/seqset.v b/util/seqset.v
index d2c6d51ef7be11290f204f3de90331b0f82e7b94..a5cc0de61e9c44eb313350f4ec35c23221742a71 100644
--- a/util/seqset.v
+++ b/util/seqset.v
@@ -1,5 +1,7 @@
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.
 
+(** In this section, we define a notion of a set (based on a sequence
+    without duplicates). *)
 Section SeqSet.
 
   (** Let [T] be any type with decidable equality. *)