aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetWeakList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
-rw-r--r--theories/FSets/FSetWeakList.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 3039c058c..866c3f620 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -807,7 +807,7 @@ Module Make (X: DecidableType) <: WS with Module E := X.
Module Raw := Raw X.
Module E := X.
- Record slist : Set := {this :> Raw.t; unique : NoDupA E.eq this}.
+ Record slist := {this :> Raw.t; unique : NoDupA E.eq this}.
Definition t := slist.
Definition elt := E.t.