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

1 files changed, 4 insertions, 9 deletions

diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index dca6e5498..579fd50c9 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -11,21 +11,16 @@
 (** * Finite map library *)  
 
 (** This file proposes an implementation of the non-dependant interface
- [FMapInterface.S] using lists of pairs,  unordered but without redundancy. *)
+ [FMapInterface.WS] using lists of pairs,  unordered but without redundancy. *)
 
-Require Import FSetInterface. 
-Require Import FSetWeakInterface.
-Require Import FMapWeakInterface.
+Require Import FMapInterface.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Arguments Scope list [type_scope].
-
 Module Raw (X:DecidableType).
 
-Module PX := KeyDecidableType X.
-Import PX.
+Module Import PX := KeyDecidableType X.
 
 Definition key := X.t.
 Definition t (elt:Set) := list (X.t * elt).
@@ -873,7 +868,7 @@ End Elt3.
 End Raw.
 
 
-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.