diff --git a/util/seqset.v b/util/seqset.v
index 4b47f7e548b807ff0835f24d68c4f0b4f58f56a3..d2c6d51ef7be11290f204f3de90331b0f82e7b94 100644
--- a/util/seqset.v
+++ b/util/seqset.v
@@ -2,17 +2,18 @@ From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.
 
 Section SeqSet.
 
-  (* Let T be any type with decidable equality. *)
-  Context {T: eqType}.
+  (** Let [T] be any type with decidable equality. *)
+  Context {T : eqType}.
 
-  (* We define a set as a sequence that has no duplicates. *)
+  (** We define a set as a sequence that has no duplicates. *)
   Record set :=
   {
     _set_seq :> seq T ;
     _ : uniq _set_seq (* no duplicates *)
   }.
 
-  (* Now we add the [ssreflect] boilerplate code. *)
+  (** Now we add the [ssreflect] boilerplate code to support [_ == _]
+      and [_ ∈ _] operations. *)
   Canonical Structure setSubType := [subType for _set_seq].
   Definition set_eqMixin := [eqMixin of set by <:].
   Canonical Structure set_eqType := EqType set set_eqMixin.
@@ -23,14 +24,15 @@ End SeqSet.
 
 Notation " {set R } " := (set_of (Phant R)).
 
+(** Next we prove a basic lemma about sets. *)
 Section Lemmas.
 
-  Context {T: eqType}.
-  Variable s: {set T}.
+  (** Consider a set [s]. *)
+  Context {T : eqType}.
+  Variable s : {set T}.
 
+  (** Then we show that element of [s] are unique. *)
   Lemma set_uniq : uniq s.
-  Proof.
-    by destruct s.
-  Qed.
+  Proof. by destruct s. Qed.
 
 End Lemmas.