From 3706139bdb4b51c1bb6c9aedab127b3b8ace62dd Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 27 Sep 2021 09:44:30 +0200
Subject: [PATCH] small clean up in util/seqset.v

---
 util/seqset.v | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/util/seqset.v b/util/seqset.v
index 4b47f7e54..d2c6d51ef 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.
-- 
GitLab