Fixing definition of set_map (bug report #2111) which was actually already

incorrect when it was introduced in 1998.  Proofs about it remain to be done...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13128 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 10 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 0ed3bbbb7..ef4933dcc 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -371,23 +371,22 @@ End first_definitions.
 
 Section other_definitions.
 
-  Variables A B : Type.
-
-  Definition set_prod : set A -> set B -> set (A * B) :=
-    list_prod (A:=A) (B:=B).
+  Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) :=
+    list_prod.
 
   (** [B^A], set of applications from [A] to [B] *)
-  Definition set_power : set A -> set B -> set (set (A * B)) :=
-    list_power (A:=A) (B:=B).
-
-  Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B).
+  Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) :=
+    list_power.
 
-  Definition set_fold_left : (B -> A -> B) -> set A -> B -> B :=
+  Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B :=
     fold_left (A:=B) (B:=A).
 
-  Definition set_fold_right (f:A -> B -> B) (x:set A)
+  Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A)
     (b:B) : B := fold_right f b x.
 
+  Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y})
+    (f : A -> B) (x : set A) : set B :=
+    set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B).
 
 End other_definitions.