diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:31:54 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:31:54 +0000 |
commit | 211030a7a870bdf3bc36b0923379e2d1bf6c729a (patch) | |
tree | 9953a1d775fe3161d43ca32e7073d10ae10349e1 /theories/FSets/FMapInterface.v | |
parent | 275151328893782671c1c6949c93b65f6d65fefa (diff) |
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
Diffstat (limited to 'theories/FSets/FMapInterface.v')
-rw-r--r-- | theories/FSets/FMapInterface.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 917534e19..ebc99933b 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -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. |