FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType

 After lots of hesitations, OrderedType now requires this "eq_dec" field, which
 is redundant (can be deduced from "compare"), but allows the subtyping relation
 DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
 extensions of weak sets. Of course this change introduces a last-minute
 incompatibility, but:

  - There is a clear gain in term of functionnality / simplicity.
  - FSets 8.2 already needs some adaptations when compared with 8.1, so it's
    the right time to push such incompatible changes.
  - Transition shouldn't be too hard: the old OrderedType still exists under
    the name MiniOrderedType, and functor MOT_to_OT allows to convert from
    one to the other.

 Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
 (resp. OrderedType), an eq_dec on sets is now required in these interfaces
 and in the implementations. In pratice, it is really easy to build from
 equal and equal_1 and equal_2.

 Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
 while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
 Idem with WDecide, WProperties and WEqProperties.

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

1 files changed, 5 insertions, 6 deletions

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 0fb41931c4..e0e8582111 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -20,11 +20,8 @@ Set Firstorder Depth 2.
 
 (** * From non-dependent signature [S] to dependent signature [Sdep]. *)
 
-Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
-  Import M.
+Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
 
-  Module ME := OrderedTypeFacts E.
-   
   Definition empty : {s : t | Empty s}.
   Proof. 
     exists empty; auto with set.
@@ -50,7 +47,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
   Proof.
     intros; exists (add x s); auto.
     unfold Add in |- *; intuition.
-    elim (ME.eq_dec x y); auto.
+    elim (E.eq_dec x y); auto.
     intros; right. 
     eapply add_3; eauto.
   Qed. 
@@ -68,7 +65,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
     intros; exists (remove x s); intuition.
     absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
-    elim (ME.eq_dec x y); intros; auto.
+    elim (E.eq_dec x y); intros; auto.
     absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
     eauto with set.
@@ -396,6 +393,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     intros; discriminate H.
   Qed.
 
+  Definition eq_dec := equal.
+
   Definition equal (s s' : t) : bool :=
     if equal s s' then true else false.