From 34a3138eaba3bfb9ef8c762fd4d056b7ddac9736 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Feb 2019 14:05:53 +0100
Subject: [PATCH] Move conversion functions list/option to set/disj_set to
 base.

---
 theories/base.v | 7 +++++++
 theories/sets.v | 7 -------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 522ef574..c0d5e898 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -868,6 +868,13 @@ Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level)
 Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
 Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
 
+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.
+
 (** The class [Lexico A] is used for the lexicographic order on [A]. This order
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
diff --git a/theories/sets.v b/theories/sets.v
index 5f65c150..0490bca5 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -748,13 +748,6 @@ End set.
 
 
 (** * Conversion of option and list *)
-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}.
   Implicit Types l : list A.
-- 
GitLab