FSetInterface: new item choose_equal in the spec S (request of P. Casteran)

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

1 files changed, 15 insertions, 2 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 9d5f2ad76..50e6fb539 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -274,8 +274,12 @@ Module Type S.
   (** Specification of [choose] *)
   Parameter choose_1 : choose s = Some x -> In x s.
   Parameter choose_2 : choose s = None -> Empty s.
-(*  Parameter choose_equal: 
-      (equal s s')=true -> E.eq (choose s) (choose s'). *)
+  Parameter choose_equal: (equal s s')=true -> 
+     match choose s, choose s' with  
+      | Some x, Some x' => E.eq x x'
+      | None, None => True
+      | _, _ => False
+     end.
 
   End Spec.
 
@@ -418,4 +422,13 @@ Module Type Sdep.
 
   Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
 
+  (** The [choose_equal] specification of [S] cannot be packed 
+        in the dependent version of [choose], so we leave it separate. *)
+  Parameter choose_equal : forall s s', Equal s s' -> 
+     match choose s, choose s' with 
+       | inleft (exist x _), inleft (exist x' _) => E.eq x x'
+       | inright _, inright _  => True
+       | _, _                        => False
+     end.
+
 End Sdep.