diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-04 17:57:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-04 17:57:01 +0000 |
| commit | fda949bd93479f8731d959133755ad08b0f9743a (patch) | |
| tree | e08ee08d2c1c314871918a586a82fb4e58cbf62a /theories/FSets/FSetWeakList.v | |
| parent | f9e40bd3cb4a71eadac0b4b8c9c376c39b29a981 (diff) | |
Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps
Thanks to Elie's work and especially "Include Type ...", full sets can
be simply expressed as extensions of weak sets. Moreover, Facts and
Properties functors can be factorized almost completely. As a result,
things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB,
Same with maps / weak maps ...
No backward compatibility intended for weak sets / maps, but porting
scripts should mostly amounts to name changes (see above).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetWeakList.v')
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index b207f1f1e..c692950e0 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -13,7 +13,7 @@ (** This file proposes an implementation of the non-dependant interface [FSetWeakInterface.S] using lists without redundancy. *) -Require Import FSetWeakInterface. +Require Import FSetInterface. Set Implicit Arguments. Unset Strict Implicit. @@ -804,7 +804,7 @@ End Raw. Now, in order to really provide a functor implementing [S], we need to encapsulate everything into a type of lists without redundancy. *) -Module Make (X: DecidableType) <: S with Module E := X. +Module Make (X: DecidableType) <: WS with Module E := X. Module Raw := Raw X. Module E := X. |