Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 3 insertions, 7 deletions

diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 1e475887..ebdc9c57 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapInterface.v 10616 2008-03-04 17:33:35Z letouzey $ *)
+(* $Id: FMapInterface.v 11699 2008-12-18 11:49:08Z letouzey $ *)
 
 (** * Finite map library *)  
 
@@ -55,11 +55,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
     No requirements for an ordering on keys nor elements, only decidability
     of equality on keys. First, a functorial signature: *)
 
-Module Type WSfun (E : EqualityType).
-
-  (** The module E of base objects is meant to be a [DecidableType]
-     (and used to be so). But requiring only an [EqualityType] here
-     allows subtyping between weak and ordered maps. *)
+Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
 
@@ -261,7 +257,7 @@ End WSfun.
     Similar to [WSfun] but expressed in a self-contained way. *)
 
 Module Type WS. 
-  Declare Module E : EqualityType.
+  Declare Module E : DecidableType.
   Include Type WSfun E.
 End WS.