Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 340 insertions, 341 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 8cb1236e..8158324e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -9,13 +8,13 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 11033 2008-06-01 22:56:50Z letouzey $ *)
+(* $Id$ *)
 
 (** * FMapAVL *)
 
 (** This module implements maps using AVL trees.
-    It follows the implementation from Ocaml's standard library. 
-    
+    It follows the implementation from Ocaml's standard library.
+
     See the comments at the beginning of FSetAVL for more details.
 *)
 
@@ -30,8 +29,8 @@ Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 
 (** * The Raw functor
-   
-   Functor of pure functions + separate proofs of invariant 
+
+   Functor of pure functions + separate proofs of invariant
    preservation *)
 
 Module Raw (Import I:Int)(X: OrderedType).
@@ -85,20 +84,20 @@ Definition is_empty m := match m with Leaf => true | _ => false end.
     to achieve logarithmic complexity. *)
 
 Fixpoint mem x m : bool :=
-   match m with 
-     |  Leaf => false 
-     |  Node l y _ r _ => match X.compare x y with 
-             | LT _ => mem x l 
+   match m with
+     |  Leaf => false
+     |  Node l y _ r _ => match X.compare x y with
+             | LT _ => mem x l
              | EQ _ => true
              | GT _ => mem x r
          end
    end.
 
-Fixpoint find x m : option elt := 
-   match m with 
-     |  Leaf => None 
-     |  Node l y d r _ => match X.compare x y with 
-             | LT _ => find x l 
+Fixpoint find x m : option elt :=
+   match m with
+     |  Leaf => None
+     |  Node l y d r _ => match X.compare x y with
+             | LT _ => find x l
              | EQ _ => Some d
              | GT _ => find x r
          end
@@ -109,7 +108,7 @@ Fixpoint find x m : option elt :=
 (** [create l x r] creates a node, assuming [l] and [r]
     to be balanced and [|height l - height r| <= 2]. *)
 
-Definition create l x e r := 
+Definition create l x e r :=
    Node l x e r (max (height l) (height r) + 1).
 
 (** [bal l x e r] acts as [create], but performs one step of
@@ -117,45 +116,45 @@ Definition create l x e r :=
 
 Definition assert_false := create.
 
-Fixpoint bal l x d r := 
-  let hl := height l in 
+Fixpoint bal l x d r :=
+  let hl := height l in
   let hr := height r in
-  if gt_le_dec hl (hr+2) then 
-    match l with 
+  if gt_le_dec hl (hr+2) then
+    match l with
      | Leaf => assert_false l x d r
-     | Node ll lx ld lr _ => 
-       if ge_lt_dec (height ll) (height lr) then 
+     | Node ll lx ld lr _ =>
+       if ge_lt_dec (height ll) (height lr) then
          create ll lx ld (create lr x d r)
-       else 
-         match lr with 
+       else
+         match lr with
           | Leaf => assert_false l x d r
-          | Node lrl lrx lrd lrr _ => 
+          | Node lrl lrx lrd lrr _ =>
               create (create ll lx ld lrl) lrx lrd (create lrr x d r)
          end
     end
-  else 
-    if gt_le_dec hr (hl+2) then 
+  else
+    if gt_le_dec hr (hl+2) then
       match r with
        | Leaf => assert_false l x d r
        | Node rl rx rd rr _ =>
-         if ge_lt_dec (height rr) (height rl) then 
+         if ge_lt_dec (height rr) (height rl) then
             create (create l x d rl) rx rd rr
-         else 
+         else
            match rl with
             | Leaf => assert_false l x d r
-            | Node rll rlx rld rlr _ => 
-                create (create l x d rll) rlx rld (create rlr rx rd rr) 
+            | Node rll rlx rld rlr _ =>
+                create (create l x d rll) rlx rld (create rlr rx rd rr)
            end
       end
-    else 
+    else
       create l x d r.
 
 (** * Insertion *)
 
-Fixpoint add x d m := 
-  match m with 
+Fixpoint add x d m :=
+  match m with
    | Leaf => Node Leaf x d Leaf 1
-   | Node l y d' r h => 
+   | Node l y d' r h =>
       match X.compare x y with
          | LT _ => bal (add x d l) y d' r
          | EQ _ => Node l y d r h
@@ -165,16 +164,16 @@ Fixpoint add x d m :=
 
 (** * Extraction of minimum binding
 
-  Morally, [remove_min] is to be applied to a non-empty tree 
-  [t = Node l x e r h]. Since we can't deal here with [assert false] 
-  for [t=Leaf], we pre-unpack [t] (and forget about [h]). 
+  Morally, [remove_min] is to be applied to a non-empty tree
+  [t = Node l x e r h]. Since we can't deal here with [assert false]
+  for [t=Leaf], we pre-unpack [t] (and forget about [h]).
 *)
- 
-Fixpoint remove_min l x d r : t*(key*elt) := 
+
+Fixpoint remove_min l x d r : t*(key*elt) :=
   match l with
     | Leaf => (r,(x,d))
-    | Node ll lx ld lr lh => 
-       let (l',m) := remove_min ll lx ld lr in 
+    | Node ll lx ld lr lh =>
+       let (l',m) := remove_min ll lx ld lr in
        (bal l' x d r, m)
   end.
 
@@ -185,18 +184,18 @@ Fixpoint remove_min l x d r : t*(key*elt) :=
   [|height t1 - height t2| <= 2].
 *)
 
-Fixpoint merge s1 s2 :=  match s1,s2 with 
-  | Leaf, _ => s2 
+Fixpoint merge s1 s2 :=  match s1,s2 with
+  | Leaf, _ => s2
   | _, Leaf => s1
-  | _, Node l2 x2 d2 r2 h2 => 
-    match remove_min l2 x2 d2 r2 with 
+  | _, Node l2 x2 d2 r2 h2 =>
+    match remove_min l2 x2 d2 r2 with
       (s2',(x,d)) => bal s1 x d s2'
     end
 end.
 
 (** * Deletion *)
 
-Fixpoint remove x m := match m with 
+Fixpoint remove x m := match m with
   | Leaf => Leaf
   | Node l y d r h =>
       match X.compare x y with
@@ -206,26 +205,26 @@ Fixpoint remove x m := match m with
       end
    end.
 
-(** * join 
-    
-    Same as [bal] but does not assume anything regarding heights of [l] 
+(** * join
+
+    Same as [bal] but does not assume anything regarding heights of [l]
     and [r].
 *)
 
 Fixpoint join l : key -> elt -> t -> t :=
   match l with
     | Leaf => add
-    | Node ll lx ld lr lh => fun x d => 
-       fix join_aux (r:t) : t := match r with 
+    | Node ll lx ld lr lh => fun x d =>
+       fix join_aux (r:t) : t := match r with
           | Leaf =>  add x d l
-          | Node rl rx rd rr rh =>  
+          | Node rl rx rd rr rh =>
                if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r)
-               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr 
+               else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr
                else create l x d r
           end
   end.
 
-(** * Splitting 
+(** * Splitting
 
     [split x m] returns a triple [(l, o, r)] where
     - [l] is the set of elements of [m] that are [< x]
@@ -236,17 +235,17 @@ Fixpoint join l : key -> elt -> t -> t :=
 Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
-Fixpoint split x m : triple := match m with 
+Fixpoint split x m : triple := match m with
   | Leaf => << Leaf, None, Leaf >>
-  | Node l y d r h => 
-     match X.compare x y with 
+  | Node l y d r h =>
+     match X.compare x y with
       | LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >>
       | EQ _ => << l, Some d, r >>
       | GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >>
      end
  end.
 
-(** * Concatenation 
+(** * Concatenation
 
    Same as [merge] but does not assume anything about heights.
 *)
@@ -256,7 +255,7 @@ Definition concat m1 m2 :=
       | Leaf, _ => m2
       | _ , Leaf => m1
       | _, Node l2 x2 d2 r2 _ =>
-            let (m2',xd) := remove_min l2 x2 d2 r2 in 
+            let (m2',xd) := remove_min l2 x2 d2 r2 in
             join m1 xd#1 xd#2 m2'
    end.
 
@@ -277,7 +276,7 @@ Definition elements := elements_aux nil.
 
 (** * Fold *)
 
-Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A := 
+Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A :=
  fun a => match m with
   | Leaf => a
   | Node l x d r _ => fold f r (f x d (fold f l a))
@@ -293,11 +292,11 @@ Inductive enumeration :=
  | End : enumeration
  | More : key -> elt -> t -> enumeration -> enumeration.
 
-(** [cons m e] adds the elements of tree [m] on the head of 
+(** [cons m e] adds the elements of tree [m] on the head of
     enumeration [e]. *)
 
-Fixpoint cons m e : enumeration := 
- match m with 
+Fixpoint cons m e : enumeration :=
+ match m with
   | Leaf => e
   | Node l x d r h => cons l (More x d r e)
  end.
@@ -316,7 +315,7 @@ Definition equal_more x1 d1 (cont:enumeration->bool) e2 :=
 
 (** Comparison of left tree, middle element, then right tree *)
 
-Fixpoint equal_cont m1 (cont:enumeration->bool) e2 := 
+Fixpoint equal_cont m1 (cont:enumeration->bool) e2 :=
  match m1 with
   | Leaf => cont e2
   | Node l1 x1 d1 r1 _ =>
@@ -341,8 +340,8 @@ Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
 
 (** * Map *)
 
-Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' := 
-  match m with 
+Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
+  match m with
    | Leaf   => Leaf _
    | Node l x d r h => Node (map f l) x (f d) (map f r) h
   end.
@@ -350,7 +349,7 @@ Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
 (* * Mapi *)
 
 Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
-  match m with 
+  match m with
    | Leaf   => Leaf _
    | Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
   end.
@@ -358,28 +357,28 @@ Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
 (** * Map with removal *)
 
 Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
-  : t elt' := 
-  match m with 
+  : t elt' :=
+  match m with
    | Leaf => Leaf _
-   | Node l x d r h => 
-      match f x d with 
+   | Node l x d r h =>
+      match f x d with
        | Some d' => join (map_option f l) x d' (map_option f r)
        | None => concat (map_option f l) (map_option f r)
       end
   end.
 
 (** * Optimized map2
-  
-  Suggestion by B. Gregoire: a [map2] function with specialized 
-  arguments allowing to bypass some tree traversal. Instead of one 
-  [f0] of type [key -> option elt -> option elt' -> option elt''], 
-  we ask here for: 
+
+  Suggestion by B. Gregoire: a [map2] function with specialized
+  arguments allowing to bypass some tree traversal. Instead of one
+  [f0] of type [key -> option elt -> option elt' -> option elt''],
+  we ask here for:
   - [f] which is a specialisation of [f0] when first option isn't [None]
   - [mapl] treats a [tree elt] with [f0] when second option is [None]
   - [mapr] treats a [tree elt'] with [f0] when first option is [None]
 
-  The idea is that [mapl] and [mapr] can be instantaneous (e.g. 
-  the identity or some constant function). 
+  The idea is that [mapl] and [mapr] can be instantaneous (e.g.
+  the identity or some constant function).
 *)
 
 Section Map2_opt.
@@ -388,13 +387,13 @@ Variable f : key -> elt -> option elt' -> option elt''.
 Variable mapl : t elt -> t elt''.
 Variable mapr : t elt' -> t elt''.
 
-Fixpoint map2_opt m1 m2 := 
- match m1, m2 with 
-  | Leaf, _ => mapr m2 
+Fixpoint map2_opt m1 m2 :=
+ match m1, m2 with
+  | Leaf, _ => mapr m2
   | _, Leaf => mapl m1
-  | Node l1 x1 d1 r1 h1, _ => 
+  | Node l1 x1 d1 r1 h1, _ =>
      let (l2',o2,r2') := split x1 m2 in
-     match f x1 d1 o2 with 
+     match f x1 d1 o2 with
       | Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2')
       | None => concat (map2_opt l1 l2') (map2_opt r1 r2')
      end
@@ -403,8 +402,8 @@ Fixpoint map2_opt m1 m2 :=
 End Map2_opt.
 
 (** * Map2
-    
-    The [map2] function of the Map interface can be implemented 
+
+    The [map2] function of the Map interface can be implemented
     via [map2_opt] and [map_option].
 *)
 
@@ -412,8 +411,8 @@ Section Map2.
 Variable elt elt' elt'' : Type.
 Variable f : option elt -> option elt' -> option elt''.
 
-Definition map2 : t elt -> t elt' -> t elt'' := 
- map2_opt 
+Definition map2 : t elt -> t elt' -> t elt'' :=
+ map2_opt
    (fun _ d o => f (Some d) o)
    (map_option (fun _ d => f (Some d) None))
    (map_option (fun _ d' => f None (Some d'))).
@@ -432,24 +431,24 @@ Variable elt : Type.
 Inductive MapsTo (x : key)(e : elt) : t elt -> Prop :=
   | MapsRoot : forall l r h y,
       X.eq x y -> MapsTo x e (Node l y e r h)
-  | MapsLeft : forall l r h y e', 
+  | MapsLeft : forall l r h y e',
       MapsTo x e l -> MapsTo x e (Node l y e' r h)
-  | MapsRight : forall l r h y e', 
+  | MapsRight : forall l r h y e',
       MapsTo x e r -> MapsTo x e (Node l y e' r h).
 
 Inductive In (x : key) : t elt -> Prop :=
   | InRoot : forall l r h y e,
       X.eq x y -> In x (Node l y e r h)
-  | InLeft : forall l r h y e', 
+  | InLeft : forall l r h y e',
       In x l -> In x (Node l y e' r h)
-  | InRight : forall l r h y e', 
+  | InRight : forall l r h y e',
       In x r -> In x (Node l y e' r h).
 
 Definition In0 k m := exists e:elt, MapsTo k e m.
 
 (** ** Binary search trees *)
 
-(** [lt_tree x s]: all elements in [s] are smaller than [x] 
+(** [lt_tree x s]: all elements in [s] are smaller than [x]
    (resp. greater for [gt_tree]) *)
 
 Definition lt_tree x m := forall y, In y m -> X.lt y x.
@@ -459,7 +458,7 @@ Definition gt_tree x m := forall y, In y m -> X.lt x y.
 
 Inductive bst : t elt -> Prop :=
   | BSLeaf : bst (Leaf _)
-  | BSNode : forall x e l r h, bst l -> bst r -> 
+  | BSNode : forall x e l r h, bst l -> bst r ->
      lt_tree x l -> gt_tree x r -> bst (Node l x e r h).
 
 End Invariants.
@@ -474,10 +473,10 @@ Module Proofs.
 
 Functional Scheme mem_ind := Induction for mem Sort Prop.
 Functional Scheme find_ind := Induction for find Sort Prop.
-Functional Scheme bal_ind := Induction for bal Sort Prop. 
+Functional Scheme bal_ind := Induction for bal Sort Prop.
 Functional Scheme add_ind := Induction for add Sort Prop.
 Functional Scheme remove_min_ind := Induction for remove_min Sort Prop.
-Functional Scheme merge_ind := Induction for merge Sort Prop. 
+Functional Scheme merge_ind := Induction for merge Sort Prop.
 Functional Scheme remove_ind := Induction for remove Sort Prop.
 Functional Scheme concat_ind := Induction for concat Sort Prop.
 Functional Scheme split_ind := Induction for split Sort Prop.
@@ -489,24 +488,24 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop.
 Hint Constructors tree MapsTo In bst.
 Hint Unfold lt_tree gt_tree.
 
-Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) 
- "as" ident(s) :=  
+Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
+ "as" ident(s) :=
  set (s:=Node l x d r h) in *; clearbody s; clear l x d r h.
 
 (** A tactic for cleaning hypothesis after use of functional induction. *)
 
 Ltac clearf :=
- match goal with 
+ match goal with
   | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
   | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
   | _ => idtac
  end.
 
-(** A tactic to repeat [inversion_clear] on all hyps of the 
+(** A tactic to repeat [inversion_clear] on all hyps of the
     form [(f (Node ...))] *)
 
 Ltac inv f :=
-  match goal with 
+  match goal with
      | H:f (Leaf _) |- _ => inversion_clear H; inv f
      | H:f _ (Leaf _) |- _ => inversion_clear H; inv f
      | H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f
@@ -518,8 +517,8 @@ Ltac inv f :=
      | _ => idtac
   end.
 
-Ltac inv_all f := 
-  match goal with 
+Ltac inv_all f :=
+  match goal with
    | H: f _ |- _ => inversion_clear H; inv f
    | H: f _ _ |- _ => inversion_clear H; inv f
    | H: f _ _ _ |- _ => inversion_clear H; inv f
@@ -529,7 +528,7 @@ Ltac inv_all f :=
 
 (** Helper tactic concerning order of elements. *)
 
-Ltac order := match goal with 
+Ltac order := match goal with
  | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
  | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
  | _ => MX.order
@@ -537,21 +536,21 @@ end.
 
 Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
 
-(* Function/Functional Scheme can't deal with internal fix. 
+(* Function/Functional Scheme can't deal with internal fix.
    Let's do its job by hand: *)
 
-Ltac join_tac := 
- intros l; induction l as [| ll _ lx ld lr Hlr lh]; 
+Ltac join_tac :=
+ intros l; induction l as [| ll _ lx ld lr Hlr lh];
    [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
-     [ | destruct (gt_le_dec lh (rh+2)); 
+     [ | destruct (gt_le_dec lh (rh+2));
        [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
-           replace (bal u v w z) 
+           replace (bal u v w z)
            with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
-         end 
-       | destruct (gt_le_dec rh (lh+2)); 
-         [ match goal with |- context [ bal ?u ?v ?w ?z ] => 
-             replace (bal u v w z) 
-             with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] 
+         end
+       | destruct (gt_le_dec rh (lh+2));
+         [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
+             replace (bal u v w z)
+             with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
            end
          | ] ] ] ]; intros.
 
@@ -575,7 +574,7 @@ Proof.
 Qed.
 
 Lemma In_alt : forall k m, In0 k m <-> In k m.
-Proof. 
+Proof.
  split.
  intros (e,H); eauto.
  unfold In0; apply In_MapsTo; auto.
@@ -588,14 +587,14 @@ Proof.
 Qed.
 Hint Immediate MapsTo_1.
 
-Lemma In_1 : 
+Lemma In_1 :
  forall m x y, X.eq x y -> In x m -> In y m.
 Proof.
  intros m x y; induction m; simpl; intuition_in; eauto.
 Qed.
 
-Lemma In_node_iff : 
- forall l x e r h y, 
+Lemma In_node_iff :
+ forall l x e r h y,
   In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r.
 Proof.
  intuition_in.
@@ -613,7 +612,7 @@ Proof.
   unfold gt_tree in |- *; intros; intuition_in.
 Qed.
 
-Lemma lt_tree_node : forall x y l r e h, 
+Lemma lt_tree_node : forall x y l r e h,
  lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h).
 Proof.
  unfold lt_tree in *; intuition_in; order.
@@ -627,25 +626,25 @@ Qed.
 
 Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 
-Lemma lt_left : forall x y l r e h, 
+Lemma lt_left : forall x y l r e h,
  lt_tree x (Node l y e r h) -> lt_tree x l.
 Proof.
  intuition_in.
 Qed.
 
-Lemma lt_right : forall x y l r e h, 
+Lemma lt_right : forall x y l r e h,
  lt_tree x (Node l y e r h) -> lt_tree x r.
 Proof.
  intuition_in.
 Qed.
 
-Lemma gt_left : forall x y l r e h, 
+Lemma gt_left : forall x y l r e h,
  gt_tree x (Node l y e r h) -> gt_tree x l.
 Proof.
  intuition_in.
 Qed.
 
-Lemma gt_right : forall x y l r e h, 
+Lemma gt_right : forall x y l r e h,
  gt_tree x (Node l y e r h) -> gt_tree x r.
 Proof.
  intuition_in.
@@ -695,39 +694,39 @@ Qed.
 
 (** * Emptyness test *)
 
-Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. 
+Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
 Proof.
  destruct m as [|r x e l h]; simpl; auto.
  intro H; elim (H x e); auto.
 Qed.
 
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
-Proof. 
+Proof.
  destruct m; simpl; intros; try discriminate; red; intuition_in.
 Qed.
 
 (** * Appartness *)
 
 Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
-Proof. 
+Proof.
  intros m x; functional induction (mem x m); auto; intros; clearf;
   inv bst; intuition_in; order.
 Qed.
 
-Lemma mem_2 : forall m x, mem x m = true -> In x m. 
-Proof. 
+Lemma mem_2 : forall m x, mem x m = true -> In x m.
+Proof.
  intros m x; functional induction (mem x m); auto; intros; discriminate.
 Qed.
 
 Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
-Proof. 
+Proof.
  intros m x; functional induction (find x m); auto; intros; clearf;
-  inv bst; intuition_in; simpl; auto; 
+  inv bst; intuition_in; simpl; auto;
  try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto].
 Qed.
 
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
-Proof. 
+Proof.
  intros m x; functional induction (find x m); subst; intros; clearf;
   try discriminate.
  constructor 2; auto.
@@ -735,7 +734,7 @@ Proof.
  constructor 3; auto.
 Qed.
 
-Lemma find_iff : forall m x e, bst m -> 
+Lemma find_iff : forall m x e, bst m ->
  (find x m = Some e <-> MapsTo x e m).
 Proof.
  split; auto using find_1, find_2.
@@ -745,7 +744,7 @@ Lemma find_in : forall m x, find x m <> None -> In x m.
 Proof.
  intros.
  case_eq (find x m); [intros|congruence].
- apply MapsTo_In with e; apply find_2; auto. 
+ apply MapsTo_In with e; apply find_2; auto.
 Qed.
 
 Lemma in_find : forall m x, bst m -> In x m -> find x m <> None.
@@ -755,7 +754,7 @@ Proof.
  rewrite (find_1 H Hd); discriminate.
 Qed.
 
-Lemma find_in_iff : forall m x, bst m -> 
+Lemma find_in_iff : forall m x, bst m ->
  (find x m <> None <-> In x m).
 Proof.
  split; auto using find_in, in_find.
@@ -771,11 +770,11 @@ Proof.
  elim H0; apply find_in; congruence.
 Qed.
 
-Lemma find_find : forall m m' x, 
- find x m = find x m' <-> 
+Lemma find_find : forall m m' x,
+ find x m = find x m' <->
  (forall d, find x m = Some d <-> find x m' = Some d).
 Proof.
- intros; destruct (find x m); destruct (find x m'); split; intros; 
+ intros; destruct (find x m); destruct (find x m'); split; intros;
   try split; try congruence.
  rewrite H; auto.
  symmetry; rewrite <- H; auto.
@@ -783,7 +782,7 @@ Proof.
 Qed.
 
 Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' ->
- (find x m = find x m' <-> 
+ (find x m = find x m' <->
   (forall d, MapsTo x d m <-> MapsTo x d m')).
 Proof.
  intros m m' x Hm Hm'.
@@ -793,8 +792,8 @@ Proof.
  rewrite 2 find_iff; auto.
 Qed.
 
-Lemma find_in_equiv : forall m m' x, bst m -> bst m' -> 
- find x m = find x m' -> 
+Lemma find_in_equiv : forall m m' x, bst m -> bst m' ->
+ find x m = find x m' ->
  (In x m <-> In x m').
 Proof.
  split; intros; apply find_in; [ rewrite <- H1 | rewrite H1 ];
@@ -803,27 +802,27 @@ Qed.
 
 (** * Helper functions *)
 
-Lemma create_bst : 
- forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
+Lemma create_bst :
+ forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r ->
  bst (create l x e r).
 Proof.
  unfold create; auto.
 Qed.
 Hint Resolve create_bst.
 
-Lemma create_in : 
- forall l x e r y,  
+Lemma create_in :
+ forall l x e r y,
   In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
  unfold create; split; [ inversion_clear 1 | ]; intuition.
 Qed.
 
-Lemma bal_bst : forall l x e r, bst l -> bst r -> 
+Lemma bal_bst : forall l x e r, bst l -> bst r ->
  lt_tree x l -> gt_tree x r -> bst (bal l x e r).
 Proof.
  intros l x e r; functional induction (bal l x e r); intros; clearf;
  inv bst; repeat apply create_bst; auto; unfold create; try constructor;
- (apply lt_tree_node || apply gt_tree_node); auto; 
+ (apply lt_tree_node || apply gt_tree_node); auto;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
 Qed.
 Hint Resolve bal_bst.
@@ -842,7 +841,7 @@ Proof.
  unfold assert_false, create; intuition_in.
 Qed.
 
-Lemma bal_find : forall l x e r y, 
+Lemma bal_find : forall l x e r y,
  bst l -> bst r -> lt_tree x l -> gt_tree x r ->
  find y (bal l x e r) = find y (create l x e r).
 Proof.
@@ -870,32 +869,32 @@ Qed.
 Hint Resolve add_bst.
 
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
-Proof. 
- intros m x y e; functional induction (add x e m); 
+Proof.
+ intros m x y e; functional induction (add x e m);
    intros; inv bst; try rewrite bal_mapsto; unfold create; eauto.
 Qed.
 
-Lemma add_2 : forall m x y e e', ~X.eq x y -> 
+Lemma add_2 : forall m x y e e', ~X.eq x y ->
  MapsTo y e m -> MapsTo y e (add x e' m).
 Proof.
  intros m x y e e'; induction m; simpl; auto.
  destruct (X.compare x k);
- intros; inv bst; try rewrite bal_mapsto; unfold create; auto; 
+ intros; inv bst; try rewrite bal_mapsto; unfold create; auto;
    inv MapsTo; auto; order.
 Qed.
 
-Lemma add_3 : forall m x y e e', ~X.eq x y -> 
+Lemma add_3 : forall m x y e e', ~X.eq x y ->
  MapsTo y e (add x e' m) -> MapsTo y e m.
 Proof.
- intros m x y e e'; induction m; simpl; auto. 
+ intros m x y e e'; induction m; simpl; auto.
  intros; inv MapsTo; auto; order.
- destruct (X.compare x k); intro; 
-  try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; 
+ destruct (X.compare x k); intro;
+  try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto;
   order.
 Qed.
 
-Lemma add_find : forall m x y e, bst m -> 
- find y (add x e m) = 
+Lemma add_find : forall m x y e, bst m ->
+ find y (add x e m) =
   match X.compare y x with EQ _ => Some e | _ => find y m end.
 Proof.
  intros.
@@ -909,7 +908,7 @@ Qed.
 (** * Extraction of minimum binding *)
 
 Lemma remove_min_in : forall l x e r h y,
- In y (Node l x e r h) <-> 
+ In y (Node l x e r h) <->
   X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1.
 Proof.
  intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
@@ -919,7 +918,7 @@ Proof.
 Qed.
 
 Lemma remove_min_mapsto : forall l x e r h y e',
-  MapsTo y e' (Node l x e r h) <-> 
+  MapsTo y e' (Node l x e r h) <->
    ((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2)
     \/ MapsTo y e' (remove_min l x e r)#1.
 Proof.
@@ -933,7 +932,7 @@ Proof.
  inversion_clear H3; intuition.
 Qed.
 
-Lemma remove_min_bst : forall l x e r h, 
+Lemma remove_min_bst : forall l x e r h,
  bst (Node l x e r h) -> bst (remove_min l x e r)#1.
 Proof.
  intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
@@ -949,8 +948,8 @@ Proof.
 Qed.
 Hint Resolve remove_min_bst.
 
-Lemma remove_min_gt_tree : forall l x e r h, 
- bst (Node l x e r h) -> 
+Lemma remove_min_gt_tree : forall l x e r h,
+ bst (Node l x e r h) ->
  gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1.
 Proof.
  intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
@@ -968,10 +967,10 @@ Proof.
 Qed.
 Hint Resolve remove_min_gt_tree.
 
-Lemma remove_min_find : forall l x e r h y, 
- bst (Node l x e r h) -> 
- find y (Node l x e r h) = 
-   match X.compare y (remove_min l x e r)#2#1 with 
+Lemma remove_min_find : forall l x e r h y,
+ bst (Node l x e r h) ->
+ find y (Node l x e r h) =
+   match X.compare y (remove_min l x e r)#2#1 with
     | LT _ => None
     | EQ _ => Some (remove_min l x e r)#2#2
     | GT _ => find y (remove_min l x e r)#1
@@ -990,9 +989,9 @@ Qed.
 
 (** * Merging two trees *)
 
-Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 -> 
+Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 ->
  (In y (merge m1 m2) <-> In y m1 \/ In y m2).
-Proof. 
+Proof.
  intros m1 m2; functional induction (merge m1 m2);intros;
   try factornode _x _x0 _x1 _x2 _x3 as m1.
  intuition_in.
@@ -1000,10 +999,10 @@ Proof.
  rewrite bal_in, remove_min_in, e1; simpl; intuition.
 Qed.
 
-Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 -> 
+Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 ->
   (MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2).
 Proof.
- intros m1 m2; functional induction (merge m1 m2); intros; 
+ intros m1 m2; functional induction (merge m1 m2); intros;
   try factornode _x _x0 _x1 _x2 _x3 as m1.
  intuition_in.
  intuition_in.
@@ -1013,12 +1012,12 @@ Proof.
  inversion_clear H1; intuition.
 Qed.
 
-Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 -> 
- (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
- bst (merge m1 m2). 
+Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 ->
+ (forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
+ bst (merge m1 m2).
 Proof.
  intros m1 m2; functional induction (merge m1 m2); intros; auto;
- try factornode _x _x0 _x1 _x2 _x3 as m1. 
+ try factornode _x _x0 _x1 _x2 _x3 as m1.
  apply bal_bst; auto.
  generalize (remove_min_bst H0); rewrite e1; simpl in *; auto.
  intro; intro.
@@ -1029,7 +1028,7 @@ Qed.
 
 (** * Deletion *)
 
-Lemma remove_in : forall m x y, bst m -> 
+Lemma remove_in : forall m x y, bst m ->
  (In y (remove x m) <-> ~ X.eq y x /\ In y m).
 Proof.
  intros m x; functional induction (remove x m); simpl; intros.
@@ -1049,7 +1048,7 @@ Proof.
 Qed.
 
 Lemma remove_bst : forall m x, bst m -> bst (remove x m).
-Proof. 
+Proof.
  intros m x; functional induction (remove x m); simpl; intros.
  auto.
  (* LT *)
@@ -1061,7 +1060,7 @@ Proof.
  (* EQ *)
  inv bst.
  apply merge_bst; eauto.
- (* GT *) 
+ (* GT *)
  inv bst.
  apply bal_bst; auto.
  intro; intro.
@@ -1070,16 +1069,16 @@ Proof.
 Qed.
 
 Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m).
-Proof. 
+Proof.
  intros; rewrite remove_in; intuition.
 Qed.
 
-Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y -> 
+Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y ->
  MapsTo y e m -> MapsTo y e (remove x m).
 Proof.
  intros m x y e; induction m; simpl; auto.
- destruct (X.compare x k); 
-   intros; inv bst; try rewrite bal_mapsto; unfold create; auto; 
+ destruct (X.compare x k);
+   intros; inv bst; try rewrite bal_mapsto; unfold create; auto;
    try solve [inv MapsTo; auto].
  rewrite merge_mapsto; auto.
  inv MapsTo; auto; order.
@@ -1089,7 +1088,7 @@ Lemma remove_3 : forall m x y e, bst m ->
  MapsTo y e (remove x m) -> MapsTo y e m.
 Proof.
  intros m x y e; induction m; simpl; auto.
- destruct (X.compare x k); intros Bs; inv bst; 
+ destruct (X.compare x k); intros Bs; inv bst;
   try rewrite bal_mapsto; auto; unfold create.
   intros; inv MapsTo; auto.
   rewrite merge_mapsto; intuition.
@@ -1098,7 +1097,7 @@ Qed.
 
 (** * join *)
 
-Lemma join_in : forall l x d r y, 
+Lemma join_in : forall l x d r y,
  In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.
  join_tac.
@@ -1110,23 +1109,23 @@ Proof.
  apply create_in.
 Qed.
 
-Lemma join_bst : forall l x d r, bst l -> bst r -> 
+Lemma join_bst : forall l x d r, bst l -> bst r ->
  lt_tree x l -> gt_tree x r -> bst (join l x d r).
 Proof.
- join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; 
+ join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto;
  clear Hrl Hlr z; intro; intros; rewrite join_in in *.
  intuition; [ apply MX.lt_eq with x | ]; eauto.
  intuition; [ apply MX.eq_lt with x | ]; eauto.
 Qed.
 Hint Resolve join_bst.
 
-Lemma join_find : forall l x d r y, 
- bst l -> bst r -> lt_tree x l -> gt_tree x r -> 
+Lemma join_find : forall l x d r y,
+ bst l -> bst r -> lt_tree x l -> gt_tree x r ->
  find y (join l x d r) = find y (create l x d r).
 Proof.
  join_tac; auto; inv bst;
-  simpl (join (Leaf elt)); 
-  try (assert (X.lt lx x) by auto); 
+  simpl (join (Leaf elt));
+  try (assert (X.lt lx x) by auto);
   try (assert (X.lt x rx) by auto);
   rewrite ?add_find, ?bal_find; auto.
 
@@ -1150,10 +1149,10 @@ Qed.
 
 (** * split *)
 
-Lemma split_in_1 : forall m x, bst m -> forall y, 
+Lemma split_in_1 : forall m x, bst m -> forall y,
  (In y (split x m)#l <-> In y m /\ X.lt y x).
 Proof.
- intros m x; functional induction (split x m); simpl; intros; 
+ intros m x; functional induction (split x m); simpl; intros;
   inv bst; try clear e0.
  intuition_in.
  rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
@@ -1162,10 +1161,10 @@ Proof.
  rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
 Qed.
 
-Lemma split_in_2 : forall m x, bst m -> forall y, 
+Lemma split_in_2 : forall m x, bst m -> forall y,
  (In y (split x m)#r <-> In y m /\ X.lt x y).
-Proof. 
- intros m x; functional induction (split x m); subst; simpl; intros; 
+Proof.
+ intros m x; functional induction (split x m); subst; simpl; intros;
   inv bst; try clear e0.
  intuition_in.
  rewrite join_in.
@@ -1174,18 +1173,18 @@ Proof.
  rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
 Qed.
 
-Lemma split_in_3 : forall m x, bst m -> 
+Lemma split_in_3 : forall m x, bst m ->
  (split x m)#o = find x m.
 Proof.
  intros m x; functional induction (split x m); subst; simpl; auto;
-  intros; inv bst; try clear e0; 
-  destruct X.compare; try (order;fail); rewrite <-IHt, e1; auto.
+  intros; inv bst; try clear e0;
+  destruct X.compare; try order; trivial; rewrite <- IHt, e1; auto.
 Qed.
 
-Lemma split_bst : forall m x, bst m -> 
+Lemma split_bst : forall m x, bst m ->
  bst (split x m)#l /\ bst (split x m)#r.
-Proof. 
- intros m x; functional induction (split x m); subst; simpl; intros; 
+Proof.
+ intros m x; functional induction (split x m); subst; simpl; intros;
   inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition;
   apply join_bst; auto.
  intros y0.
@@ -1204,17 +1203,17 @@ Proof.
  intros m x B y Hy; rewrite split_in_2 in Hy; intuition.
 Qed.
 
-Lemma split_find : forall m x y, bst m -> 
- find y m = match X.compare y x with 
+Lemma split_find : forall m x y, bst m ->
+ find y m = match X.compare y x with
               | LT _ => find y (split x m)#l
               | EQ _ => (split x m)#o
               | GT _ => find y (split x m)#r
             end.
 Proof.
- intros m x; functional induction (split x m); subst; simpl; intros; 
-  inv bst; try clear e0; try rewrite e1 in *; simpl in *; 
+ intros m x; functional induction (split x m); subst; simpl; intros;
+  inv bst; try clear e0; try rewrite e1 in *; simpl in *;
   [ destruct X.compare; auto | .. ];
-  try match goal with E:split ?x ?t = _, B:bst ?t |- _ => 
+  try match goal with E:split ?x ?t = _, B:bst ?t |- _ =>
       generalize (split_in_1 x B)(split_in_2 x B)(split_bst x B);
        rewrite E; simpl; destruct 3 end.
 
@@ -1231,7 +1230,7 @@ Qed.
 
 (** * Concatenation *)
 
-Lemma concat_in : forall m1 m2 y, 
+Lemma concat_in : forall m1 m2 y,
  In y (concat m1 m2) <-> In y m1 \/ In y m2.
 Proof.
  intros m1 m2; functional induction (concat m1 m2); intros;
@@ -1241,11 +1240,11 @@ Proof.
  rewrite join_in, remove_min_in, e1; simpl; intuition.
 Qed.
 
-Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 -> 
- (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
+Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 ->
+ (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
  bst (concat m1 m2).
 Proof.
- intros m1 m2; functional induction (concat m1 m2); intros; auto; 
+ intros m1 m2; functional induction (concat m1 m2); intros; auto;
  try factornode _x _x0 _x1 _x2 _x3 as m1.
  apply join_bst; auto.
  change (bst (m2',xd)#1); rewrite <-e1; eauto.
@@ -1256,19 +1255,19 @@ Proof.
 Qed.
 Hint Resolve concat_bst.
 
-Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> 
- (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> 
- find y (concat m1 m2) = 
+Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
+ (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
+ find y (concat m1 m2) =
   match find y m2 with Some d => Some d | None => find y m1 end.
 Proof.
- intros m1 m2; functional induction (concat m1 m2); intros; auto; 
+ intros m1 m2; functional induction (concat m1 m2); intros; auto;
  try factornode _x _x0 _x1 _x2 _x3 as m1.
  simpl; destruct (find y m2); auto.
 
  generalize (remove_min_find y H0)(remove_min_in l2 x2 d2 r2 _x4)
-  (remove_min_bst H0)(remove_min_gt_tree H0); 
+  (remove_min_bst H0)(remove_min_gt_tree H0);
   rewrite e1; simpl fst; simpl snd; intros.
- 
+
  inv bst.
  rewrite H2, join_find; auto; clear H2.
  simpl; destruct X.compare; simpl; auto.
@@ -1286,7 +1285,7 @@ Notation eqk := (PX.eqk (elt:= elt)).
 Notation eqke := (PX.eqke (elt:= elt)).
 Notation ltk := (PX.ltk (elt:= elt)).
 
-Lemma elements_aux_mapsto : forall (s:t elt) acc x e, 
+Lemma elements_aux_mapsto : forall (s:t elt) acc x e,
  InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc.
 Proof.
  induction s as [ | l Hl x e r Hr h ]; simpl; auto.
@@ -1299,8 +1298,8 @@ Proof.
  destruct H0; simpl in *; subst; intuition.
 Qed.
 
-Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. 
-Proof. 
+Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s.
+Proof.
  intros; generalize (elements_aux_mapsto s nil x e); intuition.
  inversion_clear H0.
 Qed.
@@ -1324,9 +1323,9 @@ Proof.
  induction s as [ | l Hl y e r Hr h]; simpl; intuition.
  inv bst.
  apply Hl; auto.
- constructor. 
+ constructor.
  apply Hr; eauto.
- apply (InA_InfA (PX.eqke_refl (elt:=elt))); intros (y',e') H6.
+ apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6.
  destruct (elements_aux_mapsto r acc y' e'); intuition.
  red; simpl; eauto.
  red; simpl; eauto.
@@ -1382,7 +1381,7 @@ Qed.
 
 (** * Fold *)
 
-Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) := 
+Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) :=
   L.fold f (elements s).
 
 Lemma fold_equiv_aux :
@@ -1401,14 +1400,14 @@ Lemma fold_equiv :
  forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A),
  fold f s a = fold' f s a.
 Proof.
- unfold fold', elements in |- *. 
+ unfold fold', elements in |- *.
  simple induction s; simpl in |- *; auto; intros.
  rewrite fold_equiv_aux.
  rewrite H0.
  simpl in |- *; auto.
 Qed.
 
-Lemma fold_1 : 
+Lemma fold_1 :
  forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A),
  fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i.
 Proof.
@@ -1421,9 +1420,9 @@ Qed.
 
 (** * Comparison *)
 
-(** [flatten_e e] returns the list of elements of the enumeration [e] 
+(** [flatten_e e] returns the list of elements of the enumeration [e]
     i.e. the list of elements actually compared *)
- 
+
 Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
   | End => nil
   | More x e t r => (x,e) :: elements t ++ flatten_e r
@@ -1431,13 +1430,13 @@ Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
 
 Lemma flatten_e_elements :
  forall (l:t elt) r x d z e,
- elements l ++ flatten_e (More x d r e) = 
+ elements l ++ flatten_e (More x d r e) =
  elements (Node l x d r z) ++ flatten_e e.
 Proof.
  intros; simpl; apply elements_node.
 Qed.
 
-Lemma cons_1 : forall (s:t elt) e, 
+Lemma cons_1 : forall (s:t elt) e,
   flatten_e (cons s e) = elements s ++ flatten_e e.
 Proof.
   induction s; simpl; auto; intros.
@@ -1450,24 +1449,24 @@ Variable cmp : elt->elt->bool.
 
 Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b.
 
-Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2, 
-  X.eq x1 x2 -> cmp d1 d2 = true -> 
-  IfEq b l1 l2 -> 
+Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2,
+  X.eq x1 x2 -> cmp d1 d2 = true ->
+  IfEq b l1 l2 ->
     IfEq b ((x1,d1)::l1) ((x2,d2)::l2).
 Proof.
- unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl; 
+ unfold IfEq; destruct b; simpl; intros; destruct X.compare; simpl;
   try rewrite H0; auto; order.
 Qed.
 
-Lemma equal_end_IfEq : forall e2, 
+Lemma equal_end_IfEq : forall e2,
   IfEq (equal_end e2) nil (flatten_e e2).
 Proof.
  destruct e2; red; auto.
 Qed.
 
-Lemma equal_more_IfEq : 
- forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l, 
-  IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> 
+Lemma equal_more_IfEq :
+ forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l,
+  IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
     IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l)
        (flatten_e (More x2 d2 r2 e2)).
 Proof.
@@ -1475,7 +1474,7 @@ Proof.
  rewrite <-andb_lazy_alt; f_equal; auto.
 Qed.
 
-Lemma equal_cont_IfEq : forall m1 cont e2 l, 
+Lemma equal_cont_IfEq : forall m1 cont e2 l,
   (forall e, IfEq (cont e) l (flatten_e e)) ->
   IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).
 Proof.
@@ -1493,18 +1492,18 @@ Lemma equal_IfEq : forall (m1 m2:t elt),
 Proof.
  intros; unfold equal.
  rewrite (app_nil_end (elements m1)).
- replace (elements m2) with (flatten_e (cons m2 (End _))) 
+ replace (elements m2) with (flatten_e (cons m2 (End _)))
   by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto).
  apply equal_cont_IfEq.
  intros.
  apply equal_end_IfEq; auto.
 Qed.
 
-Definition Equivb m m' := 
-  (forall k, In k m <-> In k m') /\ 
+Definition Equivb 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).
 
-Lemma Equivb_elements : forall s s', 
+Lemma Equivb_elements : forall s s',
  Equivb s s' <-> L.Equivb cmp (elements s) (elements s').
 Proof.
 unfold Equivb, L.Equivb; split; split; intros.
@@ -1516,7 +1515,7 @@ destruct H.
 apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto.
 Qed.
 
-Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' -> 
+Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' ->
   (equal cmp s s' = true <-> Equivb s s').
 Proof.
  intros s s' B B'.
@@ -1526,17 +1525,17 @@ Qed.
 
 End Elt.
 
-Section Map. 
+Section Map.
 Variable elt elt' : Type.
-Variable f : elt -> elt'. 
+Variable f : elt -> elt'.
 
-Lemma map_1 : forall (m: t elt)(x:key)(e:elt), 
+Lemma map_1 : forall (m: t elt)(x:key)(e:elt),
     MapsTo x e m -> MapsTo x (f e) (map f m).
 Proof.
 induction m; simpl; inversion_clear 1; auto.
 Qed.
 
-Lemma map_2 : forall (m: t elt)(x:key), 
+Lemma map_2 : forall (m: t elt)(x:key),
     In x (map f m) -> In x m.
 Proof.
 induction m; simpl; inversion_clear 1; auto.
@@ -1545,7 +1544,7 @@ Qed.
 Lemma map_bst : forall m, bst m -> bst (map f m).
 Proof.
 induction m; simpl; auto.
-inversion_clear 1; constructor; auto; 
+inversion_clear 1; constructor; auto;
  red; auto using map_2.
 Qed.
 
@@ -1554,7 +1553,7 @@ Section Mapi.
 Variable elt elt' : Type.
 Variable f : key -> elt -> elt'.
 
-Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), 
+Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt),
     MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
 Proof.
 induction m; simpl; inversion_clear 1; auto.
@@ -1565,7 +1564,7 @@ destruct (IHm2 _ _ H0).
 exists x0; intuition.
 Qed.
 
-Lemma mapi_2 : forall (m: t elt)(x:key), 
+Lemma mapi_2 : forall (m: t elt)(x:key),
     In x (mapi f m) -> In x m.
 Proof.
 induction m; simpl; inversion_clear 1; auto.
@@ -1574,7 +1573,7 @@ Qed.
 Lemma mapi_bst : forall m, bst m -> bst (mapi f m).
 Proof.
 induction m; simpl; auto.
-inversion_clear 1; constructor; auto; 
+inversion_clear 1; constructor; auto;
  red; auto using mapi_2.
 Qed.
 
@@ -1585,7 +1584,7 @@ Variable elt elt' : Type.
 Variable f : key -> elt -> option elt'.
 Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d.
 
-Lemma map_option_2 : forall (m:t elt)(x:key), 
+Lemma map_option_2 : forall (m:t elt)(x:key),
  In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None.
 Proof.
 intros m; functional induction (map_option f m); simpl; auto; intros.
@@ -1601,9 +1600,9 @@ Qed.
 
 Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
 Proof.
-intros m; functional induction (map_option f m); simpl; auto; intros; 
+intros m; functional induction (map_option f m); simpl; auto; intros;
  inv bst.
-apply join_bst; auto; intros y H; 
+apply join_bst; auto; intros y H;
  destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In.
 apply concat_bst; auto; intros y y' H H'.
 destruct (map_option_2 H) as (d0 & ? & ?).
@@ -1612,22 +1611,22 @@ eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
 Hint Resolve map_option_bst.
 
-Ltac nonify e := 
- replace e with (@None elt) by 
+Ltac nonify e :=
+ replace e with (@None elt) by
   (symmetry; rewrite not_find_iff; auto; intro; order).
 
-Lemma map_option_find : forall (m:t elt)(x:key), 
- bst m -> 
- find x (map_option f m) = 
+Lemma map_option_find : forall (m:t elt)(x:key),
+ bst m ->
+ find x (map_option f m) =
   match (find x m) with Some d => f x d | None => None end.
 Proof.
 intros m; functional induction (map_option f m); simpl; auto; intros;
- inv bst; rewrite join_find || rewrite concat_find; auto; simpl; 
+ inv bst; rewrite join_find || rewrite concat_find; auto; simpl;
  try destruct X.compare; simpl; auto.
 rewrite (f_compat d e); auto.
 intros y H;
  destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
-intros y H; 
+intros y H;
  destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
 
 rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto.
@@ -1653,21 +1652,21 @@ Variable mapr : t elt' -> t elt''.
 Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o.
 Hypothesis mapl_bst : forall m, bst m -> bst (mapl m).
 Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m').
-Hypothesis mapl_f0 : forall x m, bst m -> 
- find x (mapl m) = 
+Hypothesis mapl_f0 : forall x m, bst m ->
+ find x (mapl m) =
   match find x m with Some d => f0 x (Some d) None | None => None end.
-Hypothesis mapr_f0 : forall x m', bst m' -> 
- find x (mapr m') = 
+Hypothesis mapr_f0 : forall x m', bst m' ->
+ find x (mapr m') =
   match find x m' with Some d' => f0 x None (Some d') | None => None end.
 Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'.
 
 Notation map2_opt := (map2_opt f mapl mapr).
 
-Lemma map2_opt_2 : forall m m' y, bst m -> bst m' -> 
+Lemma map2_opt_2 : forall m m' y, bst m -> bst m' ->
   In y (map2_opt m m') -> In y m \/ In y m'.
 Proof.
 intros m m'; functional induction (map2_opt m m'); intros;
- auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; 
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2;
  try (generalize (split_in_1 x1 H0 y)(split_in_2 x1 H0 y)
       (split_bst x1 H0); rewrite e1; simpl; destruct 3; inv bst).
 
@@ -1689,12 +1688,12 @@ destruct (IHt1 y H6 H4 H'); intuition.
 destruct (IHt0 y H7 H5 H'); intuition.
 Qed.
 
-Lemma map2_opt_bst : forall m m', bst m -> bst m' -> 
+Lemma map2_opt_bst : forall m m', bst m -> bst m' ->
  bst (map2_opt m m').
 Proof.
 intros m m'; functional induction (map2_opt m m'); intros;
- auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst; 
- generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0); 
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; inv bst;
+ generalize (split_in_1 x1 H0)(split_in_2 x1 H0)(split_bst x1 H0);
   rewrite e1; simpl in *; destruct 3.
 
 apply join_bst; auto.
@@ -1711,31 +1710,31 @@ destruct (map2_opt_2 H2 H7 Hy'); intuition.
 Qed.
 Hint Resolve map2_opt_bst.
 
-Ltac map2_aux := 
+Ltac map2_aux :=
  match goal with
-  | H : In ?x _ \/ In ?x ?m, 
-    H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ => 
-    destruct H; [ intuition_in; order | 
+  | H : In ?x _ \/ In ?x ?m,
+    H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ =>
+    destruct H; [ intuition_in; order |
                   rewrite <-(find_in_equiv B B' H'); auto ]
  end.
 
-Ltac nonify t := 
- match t with (find ?y (map2_opt ?m ?m')) => 
+Ltac nonify t :=
+ match t with (find ?y (map2_opt ?m ?m')) =>
  replace t with (@None elt'');
  [ | symmetry; rewrite not_find_iff; auto; intro;
      destruct (@map2_opt_2 m m' y); auto; order ]
  end.
 
-Lemma map2_opt_1 : forall m m' y, bst m -> bst m' -> 
+Lemma map2_opt_1 : forall m m' y, bst m -> bst m' ->
  In y m \/ In y m' ->
  find y (map2_opt m m') = f0 y (find y m) (find y m').
 Proof.
 intros m m'; functional induction (map2_opt m m'); intros;
- auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2; 
+ auto; try factornode _x0 _x1 _x2 _x3 _x4 as m2;
  try (generalize (split_in_1 x1 H0)(split_in_2 x1 H0)
        (split_in_3 x1 H0)(split_bst x1 H0)(split_find x1 y H0)
        (split_lt_tree (x:=x1) H0)(split_gt_tree (x:=x1) H0);
-       rewrite e1; simpl in *; destruct 4; intros; inv bst; 
+       rewrite e1; simpl in *; destruct 4; intros; inv bst;
       subst o2; rewrite H7, ?join_find, ?concat_find; auto).
 
 simpl; destruct H1; [ inversion_clear H1 | ].
@@ -1777,23 +1776,23 @@ Variable f : option elt -> option elt' -> option elt''.
 Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m').
 Proof.
 unfold map2; intros.
-apply map2_opt_bst with (fun _ => f); auto using map_option_bst; 
+apply map2_opt_bst with (fun _ => f); auto using map_option_bst;
  intros; rewrite map_option_find; auto.
 Qed.
 
-Lemma map2_1 : forall m m' y, bst m -> bst m' -> 
+Lemma map2_1 : forall m m' y, bst m -> bst m' ->
   In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m').
 Proof.
 unfold map2; intros.
-rewrite (map2_opt_1 (f0:=fun _ => f)); 
+rewrite (map2_opt_1 (f0:=fun _ => f));
  auto using map_option_bst; intros; rewrite map_option_find; auto.
 Qed.
 
-Lemma map2_2 : forall m m' y, bst m -> bst m' -> 
+Lemma map2_2 : forall m m' y, bst m -> bst m' ->
   In y (map2 f m m') -> In y m \/ In y m'.
 Proof.
 unfold map2; intros.
-eapply map2_opt_2 with (f0:=fun _ => f); eauto; intros.
+eapply map2_opt_2 with (f0:=fun _ => f); try eassumption; trivial; intros.
  apply map_option_bst; auto.
  apply map_option_bst; auto.
  rewrite map_option_find; auto.
@@ -1806,38 +1805,38 @@ End Raw.
 
 (** * Encapsulation
 
-   Now, in order to really provide a functor implementing [S], we 
+   Now, in order to really provide a functor implementing [S], we
    need to encapsulate everything into a type of balanced binary search trees. *)
 
 Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Module E := X.
- Module Raw := Raw I X. 
+ Module Raw := Raw I X.
  Import Raw.Proofs.
 
- Record bst (elt:Type) := 
+ Record bst (elt:Type) :=
   Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.
- 
- Definition t := bst. 
+
+ Definition t := bst.
  Definition key := E.t.
- 
- Section Elt. 
+
+ Section Elt.
  Variable elt elt' elt'': Type.
 
  Implicit Types m : t elt.
- Implicit Types x y : key. 
- Implicit Types e : elt. 
+ Implicit Types x y : key.
+ Implicit Types e : elt.
 
  Definition empty : t elt := Bst (empty_bst elt).
  Definition is_empty m : bool := Raw.is_empty m.(this).
  Definition add x e m : t elt := Bst (add_bst x e m.(is_bst)).
- Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)). 
+ Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)).
  Definition mem x m : bool := Raw.mem x m.(this).
  Definition find x m : option elt := Raw.find x m.(this).
  Definition map f m : t elt' := Bst (map_bst f m.(is_bst)).
- Definition mapi (f:key->elt->elt') m : t elt' := 
+ Definition mapi (f:key->elt->elt') m : t elt' :=
   Bst (mapi_bst f m.(is_bst)).
- Definition map2 f m (m':t elt') : t elt'' := 
+ Definition map2 f m (m':t elt') : t elt'' :=
   Bst (map2_bst f m.(is_bst) m'.(is_bst)).
  Definition elements m : list (key*elt) := Raw.elements m.(this).
  Definition cardinal m := Raw.cardinal m.(this).
@@ -1854,14 +1853,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
  Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
- 
+
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
  Proof.
  unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
  apply m.(is_bst).
  Qed.
- 
- Lemma mem_2 : forall m x, mem x m = true -> In x m. 
+
+ Lemma mem_2 : forall m x, mem x m = true -> In x m.
  Proof.
  unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto.
  Qed.
@@ -1892,7 +1891,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed.
 
 
- Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e. 
+ Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
  Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
  Proof. intros m; exact (@find_2 elt m.(this)). Qed.
@@ -1901,36 +1900,36 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.
 
- Lemma elements_1 : forall m x e,       
+ Lemma elements_1 : forall m x e,
    MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
  Proof.
  intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto.
  Qed.
 
- Lemma elements_2 : forall m x e,   
+ Lemma elements_2 : forall m x e,
    InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
  Proof.
  intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto.
  Qed.
 
- Lemma elements_3 : forall m, sort lt_key (elements m).  
+ Lemma elements_3 : forall m, sort lt_key (elements m).
  Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.
 
- Lemma elements_3w : forall m, NoDupA eq_key (elements m).  
+ Lemma elements_3w : forall m, NoDupA eq_key (elements m).
  Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
  Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.
 
  Definition Equal m m' := forall y, find y m = find y m'.
- Definition Equiv (eq_elt:elt->elt->Prop) m m' := 
-   (forall k, In k m <-> In k m') /\ 
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
+   (forall k, In k m <-> In k m') /\
    (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
  Definition Equivb cmp := Equiv (Cmp cmp).
 
- Lemma Equivb_Equivb : forall cmp m m', 
+ Lemma Equivb_Equivb : forall cmp m m',
   Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
- Proof. 
+ Proof.
  intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.
  generalize (H0 k); do 2 rewrite In_alt; intuition.
  generalize (H0 k); do 2 rewrite In_alt; intuition.
@@ -1938,23 +1937,23 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  generalize (H0 k); do 2 rewrite <- In_alt; intuition.
  Qed.
 
- Lemma equal_1 : forall m m' cmp, 
-   Equivb cmp m m' -> equal cmp m m' = true. 
- Proof. 
- unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; 
+ Lemma equal_1 : forall m m' cmp,
+   Equivb cmp m m' -> equal cmp m m' = true.
+ Proof.
+ unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb;
   intros; simpl in *; rewrite equal_Equivb; auto.
- Qed. 
+ Qed.
 
- Lemma equal_2 : forall m m' cmp, 
+ Lemma equal_2 : forall m m' cmp,
    equal cmp m m' = true -> Equivb cmp m m'.
- Proof. 
- unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; 
+ Proof.
+ unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb;
   intros; simpl in *; rewrite <-equal_Equivb; auto.
  Qed.
 
  End Elt.
 
- Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), 
+ Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
         MapsTo x e m -> MapsTo x (f e) (map f m).
  Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.
 
@@ -1962,10 +1961,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof.
  intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl.
  apply map_2; auto.
- Qed. 
+ Qed.
 
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
-        (f:key->elt->elt'), MapsTo x e m -> 
+        (f:key->elt->elt'), MapsTo x e m ->
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
  Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
@@ -1975,10 +1974,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Qed.
 
  Lemma map2_1 : forall (elt elt' elt'':Type)(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'). 
- Proof. 
+    (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').
+ Proof.
  unfold find, map2, In; intros elt elt' elt'' m m' x f.
  do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
  apply m.(is_bst).
@@ -1986,9 +1985,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Qed.
 
  Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
-     (x:key)(f:option elt->option elt'->option elt''), 
+     (x:key)(f:option elt->option elt'->option elt''),
      In x (map2 f m m') -> In x m \/ In x m'.
- Proof. 
+ Proof.
  unfold In, map2; intros elt elt' elt'' m m' x f.
  do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
  apply m.(is_bst).
@@ -1998,19 +1997,19 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 End IntMake.
 
 
-Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: 
-    Sord with Module Data := D 
+Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
+    Sord with Module Data := D
          with Module MapS.E := X.
 
   Module Data := D.
-  Module Import MapS := IntMake(I)(X). 
+  Module Import MapS := IntMake(I)(X).
   Module LO := FMapList.Make_ord(X)(D).
   Module R := Raw.
   Module P := Raw.Proofs.
 
   Definition t := MapS.t D.t.
 
-  Definition cmp e e' := 
+  Definition cmp e e' :=
    match D.compare e e' with EQ _ => true | _ => false end.
 
   (** One step of comparison of elements *)
@@ -2020,9 +2019,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
     | R.End => Gt
     | R.More x2 d2 r2 e2 =>
        match X.compare x1 x2 with
-        | EQ _ => match D.compare d1 d2 with 
+        | EQ _ => match D.compare d1 d2 with
                    | EQ _ => cont (R.cons r2 e2)
-                   | LT _ => Lt 
+                   | LT _ => Lt
                    | GT _ => Gt
                   end
         | LT _ => Lt
@@ -2046,7 +2045,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   (** The complete comparison *)
 
-  Definition compare_pure s1 s2 := 
+  Definition compare_pure s1 s2 :=
    compare_cont s1 compare_end (R.cons s2 (Raw.End _)).
 
   (** Correctness of this comparison *)
@@ -2058,7 +2057,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
     | Gt => (fun l1 l2 => LO.lt_list l2 l1)
    end.
 
-  Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2, 
+  Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2,
    X.eq x1 x2 -> D.eq d1 d2 ->
    Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).
   Proof.
@@ -2077,10 +2076,10 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
      Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l)
        (P.flatten_e (R.More x2 d2 r2 e2)).
   Proof.
-   simpl; intros; destruct X.compare; simpl; 
+   simpl; intros; destruct X.compare; simpl;
     try destruct D.compare; simpl; auto; P.MX.elim_comp; auto.
   Qed.
-  
+
   Lemma compare_cont_Cmp : forall s1 cont e2 l,
    (forall e, Cmp (cont e) l (P.flatten_e e)) ->
    Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).
@@ -2110,14 +2109,14 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare (s s':t) : Compare lt eq s s'.
   Proof.
-   intros (s,b) (s',b').
+   destruct s as (s,b), s' as (s',b').
    generalize (compare_Cmp s s').
    destruct compare_pure; intros; [apply EQ|apply LT|apply GT]; red; auto.
   Defined.
-  
+
   (* Proofs about [eq] and [lt] *)
 
-  Definition selements (m1 : t) := 
+  Definition selements (m1 : t) :=
    LO.MapS.Build_slist (P.elements_sort m1.(is_bst)).
 
   Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
@@ -2154,7 +2153,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Qed.
 
   Lemma eq_refl : forall m : t, eq m m.
-  Proof. 
+  Proof.
   intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl.
   Qed.
 
@@ -2171,13 +2170,13 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
   Proof.
-  intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;  
+  intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;
    intros; eapply LO.lt_trans; eauto.
   Qed.
 
   Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
   Proof.
-  intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq; 
+  intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq;
    intros; apply LO.lt_not_eq; auto.
   Qed.
 
@@ -2188,8 +2187,8 @@ End IntMake_ord.
 Module Make (X: OrderedType) <: S with Module E := X
  :=IntMake(Z_as_Int)(X).
 
-Module Make_ord (X: OrderedType)(D: OrderedType) 
- <: Sord with Module Data := D 
+Module Make_ord (X: OrderedType)(D: OrderedType)
+ <: Sord with Module Data := D
             with Module MapS.E := X
  :=IntMake_ord(Z_as_Int)(X)(D).