reparation des $

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

1 files changed, 176 insertions, 176 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index ff3d7e578..ad37e0db6 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetInterface.v,v 1.11 2006/03/10 10:49:48 letouzey Exp $ *)
+(* $Id$ *)
 
 (** * Finite set library *)
 
@@ -18,12 +18,12 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
-  forall x y : A, eqA x y -> f x = f y.
+Definition compat_bool (ASet)(eqA: A->A->Prop)(f: A-> bool) :=
+  forall x y  A, eqA x y -> f x = f y.
 
 (** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) :=
-  forall x y : A, eqA x y -> P x -> P y.
+Definition compat_P (ASet)(eqA: A->A->Prop)(P : A -> Prop) :=
+  forall x y  A, eqA x y -> P x -> P y.
 
 Hint Unfold compat_bool compat_P.
 
@@ -34,243 +34,243 @@ Hint Unfold compat_bool compat_P.
 
 Module Type S.
 
-  Declare Module E : OrderedType.
-  Definition elt := E.t.
+  Declare Module E  OrderedType.
+  Definition elt = E.t.
 
-  Parameter t : Set. (** the abstract type of sets *)
+  Parameter t  Set. (** the abstract type of sets *)
 
   (** Logical predicates *)
-  Parameter In : elt -> t -> Prop.
-  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
-  Definition Subset s s' := forall a : elt, In a s -> In a s'.
-  Definition Empty s := forall a : elt, ~ In a s.
-  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
-  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+  Parameter In  elt -> t -> Prop.
+  Definition Equal s s' = forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' = forall a : elt, In a s -> In a s'.
+  Definition Empty s = forall a : elt, ~ In a s.
+  Definition For_all (P  elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P  elt -> Prop) s := exists x, In x s /\ P x.
   
-  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
-  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
+  Notation "s [=] t" = (Equal s t) (at level 70, no associativity).
+  Notation "s [<=] t" = (Subset s t) (at level 70, no associativity).
 
-  Parameter empty : t.
+  Parameter empty  t.
   (** The empty set. *)
 
-  Parameter is_empty : t -> bool.
+  Parameter is_empty  t -> bool.
   (** Test whether a set is empty or not. *)
 
-  Parameter mem : elt -> t -> bool.
+  Parameter mem  elt -> t -> bool.
   (** [mem x s] tests whether [x] belongs to the set [s]. *)
 
-  Parameter add : elt -> t -> t.
+  Parameter add  elt -> t -> t.
   (** [add x s] returns a set containing all elements of [s],
   plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
 
-  Parameter singleton : elt -> t.
+  Parameter singleton  elt -> t.
   (** [singleton x] returns the one-element set containing only [x]. *)
 
-  Parameter remove : elt -> t -> t.
+  Parameter remove  elt -> t -> t.
   (** [remove x s] returns a set containing all elements of [s],
   except [x]. If [x] was not in [s], [s] is returned unchanged. *)
 
-  Parameter union : t -> t -> t.
+  Parameter union  t -> t -> t.
   (** Set union. *)
 
-  Parameter inter : t -> t -> t.
+  Parameter inter  t -> t -> t.
   (** Set intersection. *)
 
-  Parameter diff : t -> t -> t.
+  Parameter diff  t -> t -> t.
   (** Set difference. *)
 
-  Definition eq : t -> t -> Prop := Equal.
-  Parameter lt : t -> t -> Prop.
-  Parameter compare : forall s s' : t, Compare lt eq s s'.
+  Definition eq  t -> t -> Prop := Equal.
+  Parameter lt  t -> t -> Prop.
+  Parameter compare  forall s s' : t, Compare lt eq s s'.
   (** Total ordering between sets. Can be used as the ordering function
   for doing sets of sets. *)
 
-  Parameter equal : t -> t -> bool.
+  Parameter equal  t -> t -> bool.
   (** [equal s1 s2] tests whether the sets [s1] and [s2] are
   equal, that is, contain equal elements. *)
 
-  Parameter subset : t -> t -> bool.
+  Parameter subset  t -> t -> bool.
   (** [subset s1 s2] tests whether the set [s1] is a subset of
   the set [s2]. *)
 
-  (** Coq comment: [iter] is useless in a purely functional world *)
-  (**  iter: (elt -> unit) -> set -> unit. i*)
+  (** Coq comment [iter] is useless in a purely functional world *)
+  (**  iter (elt -> unit) -> set -> unit. i*)
   (** [iter f s] applies [f] in turn to all elements of [s].
   The order in which the elements of [s] are presented to [f]
   is unspecified. *)
 
-  Parameter fold : forall A : Set, (elt -> A -> A) -> t -> A -> A.
+  Parameter fold  forall A : Set, (elt -> A -> A) -> t -> A -> A.
   (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
   where [x1 ... xN] are the elements of [s], in increasing order. *)
 
-  Parameter for_all : (elt -> bool) -> t -> bool.
+  Parameter for_all  (elt -> bool) -> t -> bool.
   (** [for_all p s] checks if all elements of the set
   satisfy the predicate [p]. *)
 
-  Parameter exists_ : (elt -> bool) -> t -> bool.
+  Parameter exists_  (elt -> bool) -> t -> bool.
   (** [exists p s] checks if at least one element of
   the set satisfies the predicate [p]. *)
 
-  Parameter filter : (elt -> bool) -> t -> t.
+  Parameter filter  (elt -> bool) -> t -> t.
   (** [filter p s] returns the set of all elements in [s]
   that satisfy predicate [p]. *)
 
-  Parameter partition : (elt -> bool) -> t -> t * t.
+  Parameter partition  (elt -> bool) -> t -> t * t.
   (** [partition p s] returns a pair of sets [(s1, s2)], where
   [s1] is the set of all the elements of [s] that satisfy the
   predicate [p], and [s2] is the set of all the elements of
   [s] that do not satisfy [p]. *)
 
-  Parameter cardinal : t -> nat.
+  Parameter cardinal  t -> nat.
   (** Return the number of elements of a set. *)
-  (** Coq comment: nat instead of int ... *)
+  (** Coq comment nat instead of int ... *)
 
-  Parameter elements : t -> list elt.
+  Parameter elements  t -> list elt.
   (** Return the list of all elements of the given set.
   The returned list is sorted in increasing order with respect
   to the ordering [Ord.compare], where [Ord] is the argument
   given to {!Set.Make}. *)
 
-  Parameter min_elt : t -> option elt.
+  Parameter min_elt  t -> option elt.
   (** Return the smallest element of the given set
   (with respect to the [Ord.compare] ordering), or raise
   [Not_found] if the set is empty. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
+  (** Coq comment [Not_found] is represented by the option type *)
 
-  Parameter max_elt : t -> option elt.
+  Parameter max_elt  t -> option elt.
   (** Same as {!Set.S.min_elt}, but returns the largest element of the
   given set. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
+  (** Coq comment [Not_found] is represented by the option type *)
 
-  Parameter choose : t -> option elt.
+  Parameter choose  t -> option elt.
   (** Return one element of the given set, or raise [Not_found] if
   the set is empty. Which element is chosen is unspecified,
   but equal elements will be chosen for equal sets. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
+  (** Coq comment [Not_found] is represented by the option type *)
 
   Section Spec. 
 
-  Variable s s' s'' : t.
-  Variable x y z : elt.
+  Variable s s' s''  t.
+  Variable x y z  elt.
 
   (** Specification of [In] *)
-  Parameter In_1 : E.eq x y -> In x s -> In y s.
+  Parameter In_1  E.eq x y -> In x s -> In y s.
  
   (** Specification of [eq] *)
-  Parameter eq_refl : eq s s. 
-  Parameter eq_sym : eq s s' -> eq s' s.
-  Parameter eq_trans : eq s s' -> eq s' s'' -> eq s s''.
+  Parameter eq_refl  eq s s. 
+  Parameter eq_sym  eq s s' -> eq s' s.
+  Parameter eq_trans  eq s s' -> eq s' s'' -> eq s s''.
  
   (** Specification of [lt] *)
-  Parameter lt_trans : lt s s' -> lt s' s'' -> lt s s''.
-  Parameter lt_not_eq : lt s s' -> ~ eq s s'.
+  Parameter lt_trans  lt s s' -> lt s' s'' -> lt s s''.
+  Parameter lt_not_eq  lt s s' -> ~ eq s s'.
 
   (** Specification of [mem] *)
-  Parameter mem_1 : In x s -> mem x s = true.
-  Parameter mem_2 : mem x s = true -> In x s. 
+  Parameter mem_1  In x s -> mem x s = true.
+  Parameter mem_2  mem x s = true -> In x s. 
  
   (** Specification of [equal] *) 
-  Parameter equal_1 : s[=]s' -> equal s s' = true.
-  Parameter equal_2 : equal s s' = true ->s[=]s'.
+  Parameter equal_1  s[=]s' -> equal s s' = true.
+  Parameter equal_2  equal s s' = true ->s[=]s'.
 
   (** Specification of [subset] *)
-  Parameter subset_1 : s[<=]s' -> subset s s' = true.
-  Parameter subset_2 : subset s s' = true -> s[<=]s'.
+  Parameter subset_1  s[<=]s' -> subset s s' = true.
+  Parameter subset_2  subset s s' = true -> s[<=]s'.
 
   (** Specification of [empty] *)
-  Parameter empty_1 : Empty empty.
+  Parameter empty_1  Empty empty.
 
   (** Specification of [is_empty] *)
-  Parameter is_empty_1 : Empty s -> is_empty s = true. 
-  Parameter is_empty_2 : is_empty s = true -> Empty s.
+  Parameter is_empty_1  Empty s -> is_empty s = true. 
+  Parameter is_empty_2  is_empty s = true -> Empty s.
  
   (** Specification of [add] *)
-  Parameter add_1 : E.eq x y -> In y (add x s).
-  Parameter add_2 : In y s -> In y (add x s).
-  Parameter add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+  Parameter add_1  E.eq x y -> In y (add x s).
+  Parameter add_2  In y s -> In y (add x s).
+  Parameter add_3  ~ E.eq x y -> In y (add x s) -> In y s. 
 
   (** Specification of [remove] *)
-  Parameter remove_1 : E.eq x y -> ~ In y (remove x s).
-  Parameter remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
-  Parameter remove_3 : In y (remove x s) -> In y s.
+  Parameter remove_1  E.eq x y -> ~ In y (remove x s).
+  Parameter remove_2  ~ E.eq x y -> In y s -> In y (remove x s).
+  Parameter remove_3  In y (remove x s) -> In y s.
 
   (** Specification of [singleton] *)
-  Parameter singleton_1 : In y (singleton x) -> E.eq x y. 
-  Parameter singleton_2 : E.eq x y -> In y (singleton x). 
+  Parameter singleton_1  In y (singleton x) -> E.eq x y. 
+  Parameter singleton_2  E.eq x y -> In y (singleton x). 
 
   (** Specification of [union] *)
-  Parameter union_1 : In x (union s s') -> In x s \/ In x s'.
-  Parameter union_2 : In x s -> In x (union s s'). 
-  Parameter union_3 : In x s' -> In x (union s s').
+  Parameter union_1  In x (union s s') -> In x s \/ In x s'.
+  Parameter union_2  In x s -> In x (union s s'). 
+  Parameter union_3  In x s' -> In x (union s s').
 
   (** Specification of [inter] *)
-  Parameter inter_1 : In x (inter s s') -> In x s.
-  Parameter inter_2 : In x (inter s s') -> In x s'.
-  Parameter inter_3 : In x s -> In x s' -> In x (inter s s').
+  Parameter inter_1  In x (inter s s') -> In x s.
+  Parameter inter_2  In x (inter s s') -> In x s'.
+  Parameter inter_3  In x s -> In x s' -> In x (inter s s').
 
   (** Specification of [diff] *)
-  Parameter diff_1 : In x (diff s s') -> In x s. 
-  Parameter diff_2 : In x (diff s s') -> ~ In x s'.
-  Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
+  Parameter diff_1  In x (diff s s') -> In x s. 
+  Parameter diff_2  In x (diff s s') -> ~ In x s'.
+  Parameter diff_3  In x s -> ~ In x s' -> In x (diff s s').
  
   (** Specification of [fold] *)  
-  Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+  Parameter fold_1  forall (A : Set) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
 
   (** Specification of [cardinal] *)  
-  Parameter cardinal_1 : cardinal s = length (elements s).
+  Parameter cardinal_1  cardinal s = length (elements s).
 
   Section Filter.
   
-  Variable f : elt -> bool.
+  Variable f  elt -> bool.
 
   (** Specification of [filter] *)
-  Parameter filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
-  Parameter filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
-  Parameter filter_3 :
+  Parameter filter_1  compat_bool E.eq f -> In x (filter f s) -> In x s. 
+  Parameter filter_2  compat_bool E.eq f -> In x (filter f s) -> f x = true. 
+  Parameter filter_3 
       compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
 
   (** Specification of [for_all] *)
-  Parameter for_all_1 :
+  Parameter for_all_1 
       compat_bool E.eq f ->
       For_all (fun x => f x = true) s -> for_all f s = true.
-  Parameter for_all_2 :
+  Parameter for_all_2 
       compat_bool E.eq f ->
       for_all f s = true -> For_all (fun x => f x = true) s.
 
   (** Specification of [exists] *)
-  Parameter exists_1 :
+  Parameter exists_1 
       compat_bool E.eq f ->
       Exists (fun x => f x = true) s -> exists_ f s = true.
-  Parameter exists_2 :
+  Parameter exists_2 
       compat_bool E.eq f ->
       exists_ f s = true -> Exists (fun x => f x = true) s.
 
   (** Specification of [partition] *)
-  Parameter partition_1 : compat_bool E.eq f -> 
+  Parameter partition_1  compat_bool E.eq f -> 
       fst (partition f s) [=] filter f s.
-  Parameter partition_2 : compat_bool E.eq f -> 
+  Parameter partition_2  compat_bool E.eq f -> 
       snd (partition f s) [=] filter (fun x => negb (f x)) s.
 
   (** 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.
-  Parameter elements_3 : sort E.lt (elements s).  
+  Parameter elements_1  In x s -> InA E.eq x (elements s).
+  Parameter elements_2  InA E.eq x (elements s) -> In x s.
+  Parameter elements_3  sort E.lt (elements s).  
 
   (** Specification of [min_elt] *)
-  Parameter min_elt_1 : min_elt s = Some x -> In x s. 
-  Parameter min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. 
-  Parameter min_elt_3 : min_elt s = None -> Empty s.
+  Parameter min_elt_1  min_elt s = Some x -> In x s. 
+  Parameter min_elt_2  min_elt s = Some x -> In y s -> ~ E.lt y x. 
+  Parameter min_elt_3  min_elt s = None -> Empty s.
 
   (** Specification of [max_elt] *)  
-  Parameter max_elt_1 : max_elt s = Some x -> In x s. 
-  Parameter max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. 
-  Parameter max_elt_3 : max_elt s = None -> Empty s.
+  Parameter max_elt_1  max_elt s = Some x -> In x s. 
+  Parameter max_elt_2  max_elt s = Some x -> In y s -> ~ E.lt x y. 
+  Parameter max_elt_3  max_elt s = None -> Empty s.
 
   (** Specification of [choose] *)
-  Parameter choose_1 : choose s = Some x -> In x s.
-  Parameter choose_2 : choose s = None -> Empty s.
-(*  Parameter choose_equal: 
+  Parameter choose_1  choose s = Some x -> In x s.
+  Parameter choose_2  choose s = None -> Empty s.
+(*  Parameter choose_equal 
       (equal s s')=true -> E.eq (choose s) (choose s'). *)
 
   End Filter.
@@ -293,124 +293,124 @@ End S.
 
 Module Type Sdep.
 
-  Declare Module E : OrderedType.
-  Definition elt := E.t.
+  Declare Module E  OrderedType.
+  Definition elt = E.t.
 
-  Parameter t : Set.
+  Parameter t  Set.
 
-  Parameter In : elt -> t -> Prop.
-  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
-  Definition Subset s s' := forall a : elt, In a s -> In a s'.
-  Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
-  Definition Empty s := forall a : elt, ~ In a s.
-  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
-  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+  Parameter In  elt -> t -> Prop.
+  Definition Equal s s' = forall a : elt, In a s <-> In a s'.
+  Definition Subset s s' = forall a : elt, In a s -> In a s'.
+  Definition Add x s s' = forall y, In y s' <-> E.eq x y \/ In y s.
+  Definition Empty s = forall a : elt, ~ In a s.
+  Definition For_all (P  elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P  elt -> Prop) s := exists x, In x s /\ P x.
 
-  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
+  Notation "s [=] t" = (Equal s t) (at level 70, no associativity).
 
-  Definition eq : t -> t -> Prop := Equal.
-  Parameter lt : t -> t -> Prop.
-  Parameter compare : forall s s' : t, Compare lt eq s s'.
+  Definition eq  t -> t -> Prop := Equal.
+  Parameter lt  t -> t -> Prop.
+  Parameter compare  forall s s' : t, Compare lt eq s s'.
 
-  Parameter eq_refl : forall s : t, eq s s. 
-  Parameter eq_sym : forall s s' : t, eq s s' -> eq s' s.
-  Parameter eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
-  Parameter lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
-  Parameter lt_not_eq : forall s s' : t, lt s s' -> ~ eq s s'.
+  Parameter eq_refl  forall s : t, eq s s. 
+  Parameter eq_sym  forall s s' : t, eq s s' -> eq s' s.
+  Parameter eq_trans  forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
+  Parameter lt_trans  forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
+  Parameter lt_not_eq  forall s s' : t, lt s s' -> ~ eq s s'.
 
-  Parameter eq_In : forall (s : t) (x y : elt), E.eq x y -> In x s -> In y s.
+  Parameter eq_In  forall (s : t) (x y : elt), E.eq x y -> In x s -> In y s.
 
-  Parameter empty : {s : t | Empty s}.
+  Parameter empty  {s : t | Empty s}.
 
-  Parameter is_empty : forall s : t, {Empty s} + {~ Empty s}.
+  Parameter is_empty  forall s : t, {Empty s} + {~ Empty s}.
 
-  Parameter mem : forall (x : elt) (s : t), {In x s} + {~ In x s}.
+  Parameter mem  forall (x : elt) (s : t), {In x s} + {~ In x s}.
 
-  Parameter add : forall (x : elt) (s : t), {s' : t | Add x s s'}.
+  Parameter add  forall (x : elt) (s : t), {s' : t | Add x s s'}.
 
   Parameter
-    singleton : forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}.
+    singleton  forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}.
   
   Parameter
-    remove :
-      forall (x : elt) (s : t),
-      {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.
+    remove 
+      forall (x  elt) (s : t),
+      {s'  t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}.
 
   Parameter
-    union :
-      forall s s' : t,
-      {s'' : t | forall x : elt, In x s'' <-> In x s \/ In x s'}.
+    union 
+      forall s s'  t,
+      {s''  t | forall x : elt, In x s'' <-> In x s \/ In x s'}.
 
   Parameter
-    inter :
-      forall s s' : t,
-      {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}.
+    inter 
+      forall s s'  t,
+      {s''  t | forall x : elt, In x s'' <-> In x s /\ In x s'}.
 
   Parameter
-    diff :
-      forall s s' : t,
-      {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.
+    diff 
+      forall s s'  t,
+      {s''  t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}.
 
-  Parameter equal : forall s s' : t, {s[=]s'} + {~ s[=]s'}.
+  Parameter equal  forall s s' : t, {s[=]s'} + {~ s[=]s'}.
  
-  Parameter subset : forall s s' : t, {Subset s s'} + {~ Subset s s'}.
+  Parameter subset  forall s s' : t, {Subset s s'} + {~ Subset s s'}.
 
   Parameter
-    filter :
-      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
-        (s : t),
-      {s' : t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}.
+    filter 
+      forall (P  elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s  t),
+      {s'  t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}.
 
   Parameter
-    for_all :
-      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
-        (s : t),
+    for_all 
+      forall (P  elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s  t),
       {compat_P E.eq P -> For_all P s} + {compat_P E.eq P -> ~ For_all P s}.
   
   Parameter
-    exists_ :
-      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
-        (s : t),
+    exists_ 
+      forall (P  elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s  t),
       {compat_P E.eq P -> Exists P s} + {compat_P E.eq P -> ~ Exists P s}.
 
   Parameter
-    partition :
-      forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
-        (s : t),
-      {partition : t * t |
-      let (s1, s2) := partition in
+    partition 
+      forall (P  elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x})
+        (s  t),
+      {partition  t * t |
+      let (s1, s2) = partition in
       compat_P E.eq P ->
       For_all P s1 /\
       For_all (fun x => ~ P x) s2 /\
-      (forall x : elt, In x s <-> In x s1 \/ In x s2)}.
+      (forall x  elt, In x s <-> In x s1 \/ In x s2)}.
 
   Parameter
-    elements :
-      forall s : t,
-      {l : list elt |
-      sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}.
+    elements 
+      forall s  t,
+      {l  list elt |
+      sort E.lt l /\ (forall x  elt, In x s <-> InA E.eq x l)}.
 
   Parameter
-    fold :
-      forall (A : Set) (f : elt -> A -> A) (s : t) (i : A),
-      {r : A | let (l,_) := elements s in 
+    fold 
+      forall (A  Set) (f : elt -> A -> A) (s : t) (i : A),
+      {r  A | let (l,_) := elements s in 
                   r = fold_left (fun a e => f e a) l i}.
 
   Parameter
-    cardinal :
-      forall s : t,
-      {r : nat | let (l,_) := elements s in r = length l }.
+    cardinal 
+      forall s  t,
+      {r  nat | let (l,_) := elements s in r = length l }.
 
   Parameter
-    min_elt :
-      forall s : t,
-      {x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.
+    min_elt 
+      forall s  t,
+      {x  elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}.
 
   Parameter
-    max_elt :
-      forall s : t,
-      {x : elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}.
+    max_elt 
+      forall s  t,
+      {x  elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}.
 
-  Parameter choose : forall s : t, {x : elt | In x s} + {Empty s}.
+  Parameter choose  forall s : t, {x : elt | In x s} + {Empty s}.
 
 End Sdep.