From d9fe131bd3df997bc5758cf484bc2d2b1d908702 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 2 Nov 2021 09:46:32 +0100
Subject: [PATCH] add comment in util/seqset

---
 util/seqset.v | 2 ++
 1 file changed, 2 insertions(+)

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