From 9b98b7ba5470edfbe5255fbe4e32e13c50fa64c1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 28 Feb 2008 00:20:33 +0000
Subject: Nicer third spec of choose. The old version is now a properties in
 FSetProperties.OrdProperties

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetInterface.v | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'theories/FSets/FSetInterface.v')

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index c113a7d242..eb2a730868 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -338,12 +338,8 @@ Module Type Sfun (E : OrderedType).
   Parameter max_elt_3 : max_elt s = None -> Empty s.
 
   (** Additional specification of [choose] *)
-  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.
+  Parameter choose_3 : choose s = Some x -> choose s' = Some y -> 
+    Equal s s' -> E.eq x y.
 
   End Spec.
 
@@ -507,7 +503,7 @@ Module Type Sdep.
 
   Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
 
-  (** The [choose_equal] specification of [S] cannot be packed 
+  (** The [choose_3] 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 
-- 
cgit v1.2.3