From 45ae06c795f80d8b53b8c0a1db2a55c0185a7968 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 Feb 2019 10:09:10 +0100
Subject: [PATCH] add list_to_set_disj (replacing the list_to_set on gmultiset)

---
 theories/sets.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/sets.v b/theories/sets.v
index e1d9d1c6..5f65c150 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -752,6 +752,8 @@ Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
 Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
   match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end.
+Fixpoint list_to_set_disj `{Singleton A C, Empty C, DisjUnion C} (l : list A) : C :=
+  match l with [] => ∅ | x :: l => {[ x ]} ⊎ list_to_set_disj l end.
 
 Section option_and_list_to_set.
   Context `{SemiSet A C}.
-- 
GitLab