From efc09aa417b49315aa9e1fea1a13987241d3752a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 20 Oct 2009 11:49:19 +0000
Subject: 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
---
 theories/Structures/DecidableType2.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'theories/Structures/DecidableType2.v')

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).
-- 
cgit v1.2.3