3*rien

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

2 files changed, 7 insertions, 5 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 3868e84ce..9d5f2ad76 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -153,7 +153,7 @@ Module Type S.
   Section Spec. 
 
   Variable s s' s'' : t.
-  Variable x y z : elt.
+  Variable x y : elt.
 
   (** Specification of [In] *)
   Parameter In_1 : E.eq x y -> In x s -> In y s.
@@ -254,6 +254,8 @@ Module Type S.
   Parameter partition_2 : compat_bool E.eq f -> 
       snd (partition f s) [=] filter (fun x => negb (f x)) s.
 
+  End Filter.
+
   (** Specification of [elements] *)
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
@@ -275,7 +277,6 @@ Module Type S.
 (*  Parameter choose_equal: 
       (equal s s')=true -> E.eq (choose s) (choose s'). *)
 
-  End Filter.
   End Spec.
 
   (* begin hide *)
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 27e4a5ccf..81d148b4e 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -132,8 +132,8 @@ Module Type S.
 
   Section Spec. 
 
-  Variable s s' s'' : t.
-  Variable x y z : elt.
+  Variable s s' : t.
+  Variable x y : elt.
 
   (** Specification of [In] *)
   Parameter In_1 : E.eq x y -> In x s -> In y s.
@@ -226,6 +226,8 @@ Module Type S.
       compat_bool E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
 
+  End Filter.
+
   (** Specification of [elements] *)
   Parameter elements_1 : In x s -> InA E.eq x (elements s).
   Parameter elements_2 : InA E.eq x (elements s) -> In x s.
@@ -235,7 +237,6 @@ Module Type S.
   Parameter choose_1 : choose s = Some x -> In x s.
   Parameter choose_2 : choose s = None -> Empty s.
 
-  End Filter.
   End Spec.
 
   Hint Immediate In_1.