Réparation de FSet (back to 8628)

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

1 files changed, 81 insertions, 81 deletions

diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 2ab0a0d8d..828f5dc05 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id$ *)
+(* $Id: FMapInterface.v,v 1.13 2006/02/27 15:39:43 letouzey Exp $ *)
 
 (** * Finite map library *)  
 
@@ -17,7 +17,7 @@ Unset Strict Implicit.
 Require Import FSetInterface. 
 
 
-(** When compared with Ocaml Map, this signature has been split in two 
+(** When compared with Ocaml Map, this signature has been split in two: 
    - The first part [S] contains the usual operators (add, find, ...)
      It only requires a ordered key type, the data type can be arbitrary. 
      The only function that asks more is [equal], whose first argument should 
@@ -29,81 +29,81 @@ Require Import FSetInterface.
 
 Module Type S.
 
-  Declare Module E  OrderedType.
+  Declare Module E : OrderedType.
 
-  Definition key = E.t.
+  Definition key := E.t.
 
-  Parameter t  Set -> Set. (** the abstract type of maps *)
+  Parameter t : Set -> Set. (** the abstract type of maps *)
  
   Section Types. 
 
-    Variable eltSet.
+    Variable elt:Set.
 
-    Parameter empty  t elt.
+    Parameter empty : t elt.
       (** The empty map. *)
 
-    Parameter is_empty  t elt -> bool.
+    Parameter is_empty : t elt -> bool.
     (** Test whether a map is empty or not. *)
 
-    Parameter add  key -> elt -> t elt -> t elt.
+    Parameter add : key -> elt -> t elt -> t elt.
     (** [add x y m] returns a map containing the same bindings as [m], 
 	plus a binding of [x] to [y]. If [x] was already bound in [m], 
 	its previous binding disappears. *)
 
-    Parameter find  key -> t elt -> option elt. 
+    Parameter find : key -> t elt -> option elt. 
     (** [find x m] returns the current binding of [x] in [m], 
 	or raises [Not_found] if no such binding exists.
-	NB in Coq, the exception mechanism becomes a option type. *)
+	NB: in Coq, the exception mechanism becomes a option type. *)
 
-    Parameter remove  key -> t elt -> t elt.
+    Parameter remove : key -> t elt -> t elt.
     (** [remove x m] returns a map containing the same bindings as [m], 
 	except for [x] which is unbound in the returned map. *)
 
-    Parameter mem  key -> t elt -> bool.
+    Parameter mem : key -> t elt -> bool.
     (** [mem x m] returns [true] if [m] contains a binding for [x], 
 	and [false] otherwise. *)
 
-    (** Coq comment [iter] is useless in a purely functional world *)
-    (** val iter  (key -> 'a -> unit) -> 'a t -> unit *)
+    (** Coq comment: [iter] is useless in a purely functional world *)
+    (** val iter : (key -> 'a -> unit) -> 'a t -> unit *)
     (** iter f m applies f to all bindings in map m. f receives the key as 
 	first argument, and the associated value as second argument. 
 	The bindings are passed to f in increasing order with respect to the 
 	ordering over the type of the keys. Only current bindings are 
-	presented to f bindings hidden by more recent bindings are not 
+	presented to f: bindings hidden by more recent bindings are not 
 	passed to f. *)
 
-    Variable elt'  Set. 
-    Variable elt'' Set.
+    Variable elt' : Set. 
+    Variable elt'': Set.
 
-    Parameter map  (elt -> elt') -> t elt -> t elt'.
+    Parameter map : (elt -> elt') -> t elt -> t elt'.
     (** [map f m] returns a map with same domain as [m], where the associated 
 	value a of all bindings of [m] has been replaced by the result of the
 	application of [f] to [a]. The bindings are passed to [f] in 
 	increasing order with respect to the ordering over the type of the 
 	keys. *)
 
-    Parameter mapi  (key -> elt -> elt') -> t elt -> t elt'.
+    Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
     (** Same as [S.map], but the function receives as arguments both the 
 	key and the associated value for each binding of the map. *)
 
-    Parameter map2  (option elt -> option elt' -> option elt'') -> t elt -> t elt' ->  t elt''.
+    Parameter map2 : (option elt -> option elt' -> option elt'') -> t elt -> t elt' ->  t elt''.
     (** Not present in Ocaml. 
          [map f m m'] creates a new map whose bindings belong to the ones of either 
          [m] or [m']. The presence and value for a key [k] is determined by [f e e'] 
          where [e] and [e'] are the (optional) bindings of [k] in [m] and [m']. *)
 
-    Parameter elements  t elt -> list (key*elt).
+    Parameter elements : t elt -> list (key*elt).
     (** Not present in Ocaml. 
          [elements m] returns an assoc list corresponding to the bindings of [m].
          Elements of this list are sorted with respect to their first components. 
          Useful to specify [fold] ... *)
 
-    Parameter fold  forall A: Set, (key -> elt -> A -> A) -> t elt -> A -> A.
+    Parameter fold : forall A: Set, (key -> elt -> A -> A) -> t elt -> A -> A.
     (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
 	where [k1] ... [kN] are the keys of all bindings in [m] 
 	(in increasing order), and [d1] ... [dN] are the associated data. *)
 
-    Parameter equal  (elt -> elt -> bool) -> t elt -> t elt -> bool.
+    Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
     (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal, 
       that is, contain equal keys and associate them with equal data. 
       [cmp] is the equality predicate used to compare the data associated 
@@ -111,97 +111,97 @@ Module Type S.
 
     Section Spec. 
       
-      Variable m m' m''  t elt.
-      Variable x y z  key.
-      Variable e e'  elt.
+      Variable m m' m'' : t elt.
+      Variable x y z : key.
+      Variable e e' : elt.
 
-      Parameter MapsTo  key -> elt -> t elt -> Prop.
+      Parameter MapsTo : key -> elt -> t elt -> Prop.
 
-      Definition In (kkey)(m: t elt) : Prop := exists e:elt, MapsTo k e m.
+      Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.
 
-      Definition Empty m = forall (a : key)(e:elt) , ~ MapsTo a e m.
+      Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m.
 
-      Definition eq_key (p p'key*elt) := E.eq (fst p) (fst p').
+      Definition eq_key (p p':key*elt) := E.eq (fst p) (fst p').
       
-      Definition eq_key_elt (p p'key*elt) := 
+      Definition eq_key_elt (p p':key*elt) := 
           E.eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-      Definition lt_key (p p'key*elt) := E.lt (fst p) (fst p').
+      Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
 
     (** Specification of [MapsTo] *)
-      Parameter MapsTo_1  E.eq x y -> MapsTo x e m -> MapsTo y e m.
+      Parameter MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m.
       
     (** Specification of [mem] *)
-      Parameter mem_1  In x m -> mem x m = true.
-      Parameter mem_2  mem x m = true -> In x m. 
+      Parameter mem_1 : In x m -> mem x m = true.
+      Parameter mem_2 : mem x m = true -> In x m. 
       
     (** Specification of [empty] *)
-      Parameter empty_1  Empty empty.
+      Parameter empty_1 : Empty empty.
 
     (** Specification of [is_empty] *)
-      Parameter is_empty_1  Empty m -> is_empty m = true. 
-      Parameter is_empty_2  is_empty m = true -> Empty m.
+      Parameter is_empty_1 : Empty m -> is_empty m = true. 
+      Parameter is_empty_2 : is_empty m = true -> Empty m.
       
     (** Specification of [add] *)
-      Parameter add_1  E.eq x y -> MapsTo y e (add x e m).
-      Parameter add_2  ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
-      Parameter add_3  ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
+      Parameter add_1 : E.eq x y -> MapsTo y e (add x e m).
+      Parameter add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
+      Parameter add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
 
     (** Specification of [remove] *)
-      Parameter remove_1  E.eq x y -> ~ In y (remove x m).
-      Parameter remove_2  ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
-      Parameter remove_3  MapsTo y e (remove x m) -> MapsTo y e m.
+      Parameter remove_1 : E.eq x y -> ~ In y (remove x m).
+      Parameter remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
+      Parameter remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
 
     (** Specification of [find] *)
-      Parameter find_1  MapsTo x e m -> find x m = Some e. 
-      Parameter find_2  find x m = Some e -> MapsTo x e m.
+      Parameter find_1 : MapsTo x e m -> find x m = Some e. 
+      Parameter find_2 : find x m = Some e -> MapsTo x e m.
 
     (** Specification of [elements] *)
-      Parameter elements_1  
+      Parameter elements_1 : 
         MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
-      Parameter elements_2  
+      Parameter elements_2 : 
         InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
-      Parameter elements_3  sort lt_key (elements m).  
+      Parameter elements_3 : sort lt_key (elements m).  
 
     (** Specification of [fold] *)  
-      Parameter fold_1 
-	forall (A  Set) (i : A) (f : key -> elt -> A -> A),
+      Parameter fold_1 :
+	forall (A : Set) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  
-   Definition Equal cmp m m' = 
+   Definition Equal cmp m m' := 
          (forall k, In k m <-> In k m') /\ 
          (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).  
 
-   Variable cmp  elt -> elt -> bool. 
+   Variable cmp : elt -> elt -> bool. 
 
    (** Specification of [equal] *)
-     Parameter equal_1  Equal cmp m m' -> equal cmp m m' = true. 
-     Parameter equal_2  equal cmp m m' = true -> Equal cmp m m'.
+     Parameter equal_1 : Equal cmp m m' -> equal cmp m m' = true. 
+     Parameter equal_2 : equal cmp m m' = true -> Equal cmp m m'.
 
     End Spec. 
    End Types. 
 
     (** Specification of [map] *)
-      Parameter map_1  forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
+      Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
         MapsTo x e m -> MapsTo x (f e) (map f m).
-      Parameter map_2  forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), 
+      Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), 
         In x (map f m) -> In x m.
  
     (** Specification of [mapi] *)
-      Parameter mapi_1  forall (elt elt':Set)(m: t elt)(x:key)(e:elt)
-        (fkey->elt->elt'), MapsTo x e m -> 
+      Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)
+        (f:key->elt->elt'), MapsTo x e m -> 
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
-      Parameter mapi_2  forall (elt elt':Set)(m: t elt)(x:key)
-        (fkey->elt->elt'), In x (mapi f m) -> In x m.
+      Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key)
+        (f:key->elt->elt'), In x (mapi f m) -> In x m.
 
     (** Specification of [map2] *)
-      Parameter map2_1  forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
-	(xkey)(f:option elt->option elt'->option elt''), 
+      Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
+	(x:key)(f:option elt->option elt'->option elt''), 
 	In x m \/ In x m' -> 
         find x (map2 f m m') = f (find x m) (find x m').       
 
-     Parameter map2_2  forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
-	(xkey)(f:option elt->option elt'->option elt''), 
+     Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt')
+	(x:key)(f:option elt->option elt'->option elt''), 
         In x (map2 f m m') -> In x m \/ In x m'.
 
   Hint Immediate MapsTo_1 mem_2 is_empty_2.
@@ -214,28 +214,28 @@ End S.
 
 Module Type Sord.
  
-  Declare Module Data  OrderedType.   
-  Declare Module MapS  S. 
+  Declare Module Data : OrderedType.   
+  Declare Module MapS : S. 
   Import MapS.
   
-  Definition t = MapS.t Data.t. 
+  Definition t := MapS.t Data.t. 
 
-  Parameter eq  t -> t -> Prop.
-  Parameter lt  t -> t -> Prop. 
+  Parameter eq : t -> t -> Prop.
+  Parameter lt : t -> t -> Prop. 
  
-  Axiom eq_refl  forall m : t, eq m m.
-  Axiom eq_sym  forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
-  Axiom eq_trans  forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
-  Axiom lt_trans  forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
-  Axiom lt_not_eq  forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
+  Axiom eq_refl : forall m : t, eq m m.
+  Axiom eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
+  Axiom eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
+  Axiom lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
+  Axiom lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
 
-  Definition cmp e e' = match Data.compare e e' with Eq _ => true | _ => false end.	
+  Definition cmp e e' := match Data.compare e e' with Eq _ => true | _ => false end.	
 
-  Parameter eq_1  forall m m', Equal cmp m m' -> eq m m'.
-  Parameter eq_2  forall m m', eq m m' -> Equal cmp m m'.
+  Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'.
+  Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'.
 
-  Parameter compare  forall m1 m2, Compare lt eq m1 m2.
-  (** Total ordering between maps. The first argument (in Coq Data.compare) 
+  Parameter compare : forall m1 m2, Compare lt eq m1 m2.
+  (** Total ordering between maps. The first argument (in Coq: Data.compare) 
       is a total ordering used to compare data associated with equal keys 
       in the two maps. *)