FSetCompat: a compatibility wrapper between FSets and MSets

 Thanks to the functors in FSetCompat, the three implementations
 of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few
 lines adapting the corresponding MSets implementation to the old
 interface.

 This approach breaks FSetFullAVL. Since this file is of little use
 for stdlib users, we migrate it into contrib Orsay/FSets.

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

1 files changed, 20 insertions, 0 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index c6d16a6c56..61fd743dc3 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -9,6 +9,8 @@
 (* $Id$ *)
 
 Require Export SetoidList.
+Require DecidableType. (* No Import here, this is on purpose *)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -31,6 +33,24 @@ Module Type DecidableType.
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
 End DecidableType.
 
+(** * Compatibility wrapper from/to the old version of [DecidableType] *)
+
+Module Type DecidableTypeOrig := DecidableType.DecidableType.
+
+Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
+ Include E.
+ Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+End Backport_DT.
+
+Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
+ Include E.
+ Instance eq_equiv : Equivalence eq.
+ Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed.
+End Update_DT.
+
+
 (** * Additional notions about keys and datas used in FMap *)
 
 Module KeyDecidableType(D:DecidableType).