1 files changed, 138 insertions, 137 deletions

diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 57cbbcc4..e4f8b4df 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -1,4 +1,3 @@
-
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -9,26 +8,26 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapFullAVL.v 10748 2008-04-03 18:28:26Z letouzey $ *)
+(* $Id$ *)
 
 (** * FMapFullAVL
-   
+
    This file contains some complements to [FMapAVL].
 
-   - Functor [AvlProofs] proves that trees of [FMapAVL] are not only 
+   - Functor [AvlProofs] proves that trees of [FMapAVL] are not only
    binary search trees, but moreover well-balanced ones. This is done
    by proving that all operations preserve the balancing.
-  
-   - We then pack the previous elements in a [IntMake] functor 
+
+   - We then pack the previous elements in a [IntMake] functor
    similar to the one of [FMapAVL], but richer.
 
-   - In final [IntMake_ord] functor, the [compare] function is 
-   different from the one in [FMapAVL]: this non-structural 
+   - In final [IntMake_ord] functor, the [compare] function is
+   different from the one in [FMapAVL]: this non-structural
    version is closer to the original Ocaml code.
 
 *)
 
-Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL.
+Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -40,6 +39,8 @@ Import Raw.Proofs.
 Open Local Scope pair_scope.
 Open Local Scope Int_scope.
 
+Ltac omega_max := i2z_refl; romega with Z.
+
 Section Elt.
 Variable elt : Type.
 Implicit Types m r : t elt.
@@ -52,11 +53,11 @@ Implicit Types m r : t elt.
 
 Inductive avl : t elt -> Prop :=
   | RBLeaf : avl (Leaf _)
-  | RBNode : forall x e l r h, 
+  | RBNode : forall x e l r h,
       avl l ->
       avl r ->
       -(2) <= height l - height r <= 2 ->
-      h = max (height l) (height r) + 1 -> 
+      h = max (height l) (height r) + 1 ->
       avl (Node l x e r h).
 
 
@@ -64,28 +65,28 @@ Inductive avl : t elt -> Prop :=
 
 Hint Constructors avl.
 
-Lemma height_non_negative : forall (s : t elt), avl s -> 
+Lemma height_non_negative : forall (s : t elt), avl s ->
  height s >= 0.
 Proof.
  induction s; simpl; intros; auto with zarith.
  inv avl; intuition; omega_max.
 Qed.
 
-Ltac avl_nn_hyp H := 
+Ltac avl_nn_hyp H :=
      let nz := fresh "nz" in assert (nz := height_non_negative H).
 
-Ltac avl_nn h := 
-  let t := type of h in 
-  match type of t with 
+Ltac avl_nn h :=
+  let t := type of h in
+  match type of t with
    | Prop => avl_nn_hyp h
    | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
   end.
 
-(* Repeat the previous tactic. 
+(* Repeat the previous tactic.
    Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)
 
 Ltac avl_nns :=
-  match goal with 
+  match goal with
      | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
      | _ => idtac
   end.
@@ -103,49 +104,49 @@ Hint Resolve avl_node.
 
 (** Results about [height] *)
 
-Lemma height_0 : forall l, avl l -> height l = 0 -> 
+Lemma height_0 : forall l, avl l -> height l = 0 ->
  l = Leaf _.
 Proof.
  destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; elimtype False; omega_max.
+ avl_nns; simpl in *; exfalso; omega_max.
 Qed.
 
 
 (** * Empty map *)
 
 Lemma empty_avl : avl (empty elt).
-Proof. 
+Proof.
  unfold empty; auto.
 Qed.
 
 
 (** * Helper functions *)
 
-Lemma create_avl : 
- forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
+Lemma create_avl :
+ forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
  avl (create l x e r).
 Proof.
  unfold create; auto.
 Qed.
 
-Lemma create_height : 
- forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 -> 
+Lemma create_height :
+ forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
  height (create l x e r) = max (height l) (height r) + 1.
 Proof.
  unfold create; intros; auto.
 Qed.
 
-Lemma bal_avl : forall l x e r, avl l -> avl r -> 
+Lemma bal_avl : forall l x e r, avl l -> avl r ->
  -(3) <= height l - height r <= 3 -> avl (bal l x e r).
 Proof.
  intros l x e r; functional induction (bal l x e r); intros; clearf;
- inv avl; simpl in *; 
+ inv avl; simpl in *;
  match goal with |- avl (assert_false _ _ _ _) => avl_nns
   | _ => repeat apply create_avl; simpl in *; auto
  end; omega_max.
 Qed.
 
-Lemma bal_height_1 : forall l x e r, avl l -> avl r -> 
+Lemma bal_height_1 : forall l x e r, avl l -> avl r ->
  -(3) <= height l - height r <= 3 ->
  0 <= height (bal l x e r) - max (height l) (height r) <= 1.
 Proof.
@@ -153,25 +154,25 @@ Proof.
  inv avl; avl_nns; simpl in *; omega_max.
 Qed.
 
-Lemma bal_height_2 : 
- forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> 
+Lemma bal_height_2 :
+ forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
  height (bal l x e r) == max (height l) (height r) +1.
 Proof.
  intros l x e r; functional induction (bal l x e r); intros; clearf;
  inv avl; avl_nns; simpl in *; omega_max.
 Qed.
 
-Ltac omega_bal := match goal with 
-  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] => 
-     generalize (bal_height_1 x e H H') (bal_height_2 x e H H'); 
+Ltac omega_bal := match goal with
+  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] =>
+     generalize (bal_height_1 x e H H') (bal_height_2 x e H H');
      omega_max
   end.
 
 (** * Insertion *)
 
-Lemma add_avl_1 :  forall m x e, avl m -> 
+Lemma add_avl_1 :  forall m x e, avl m ->
  avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
-Proof. 
+Proof.
  intros m x e; functional induction (add x e m); intros; inv avl; simpl in *.
  intuition; try constructor; simpl; auto; try omega_max.
  (* LT *)
@@ -196,8 +197,8 @@ Hint Resolve add_avl.
 
 (** * Extraction of minimum binding *)
 
-Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) -> 
- avl (remove_min l x e r)#1 /\ 
+Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) ->
+ avl (remove_min l x e r)#1 /\
  0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.
 Proof.
  intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.
@@ -210,20 +211,20 @@ Proof.
  omega_bal.
 Qed.
 
-Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) -> 
-    avl (remove_min l x e r)#1. 
+Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) ->
+    avl (remove_min l x e r)#1.
 Proof.
  intros; generalize (remove_min_avl_1 H); intuition.
 Qed.
 
 (** * Merging two trees *)
 
-Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 -> 
- -(2) <= height m1 - height m2 <= 2 -> 
- avl (merge m1 m2) /\ 
+Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 ->
+ -(2) <= height m1 - height m2 <= 2 ->
+ avl (merge m1 m2) /\
  0<= height (merge m1 m2) - max (height m1) (height m2) <=1.
 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.
  simpl; split; auto; avl_nns; omega_max.
  simpl; split; auto; avl_nns; omega_max.
@@ -235,16 +236,16 @@ Proof.
  omega_bal.
 Qed.
 
-Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 -> 
+Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 ->
   -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2).
-Proof. 
+Proof.
  intros; generalize (merge_avl_1 H H0 H1); intuition.
 Qed.
 
 
 (** * Deletion *)
 
-Lemma remove_avl_1 : forall m x, avl m -> 
+Lemma remove_avl_1 : forall m x, avl m ->
  avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1.
 Proof.
  intros m x; functional induction (remove x m); intros.
@@ -252,25 +253,25 @@ Proof.
  (* LT *)
  inv avl.
  destruct (IHt H0).
- split. 
+ split.
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
- inv avl. 
+ inv avl.
  generalize (merge_avl_1 H0 H1 H2).
  intuition omega_max.
  (* GT *)
  inv avl.
  destruct (IHt H1).
- split. 
+ split.
  apply bal_avl; auto.
  omega_max.
  omega_bal.
 Qed.
 
 Lemma remove_avl : forall m x, avl m -> avl (remove x m).
-Proof. 
+Proof.
  intros; generalize (remove_avl_1 x H); intuition.
 Qed.
 Hint Resolve remove_avl.
@@ -278,7 +279,7 @@ Hint Resolve remove_avl.
 
 (** * Join *)
 
-Lemma join_avl_1 : forall l x d r, avl l -> avl r -> 
+Lemma join_avl_1 : forall l x d r, avl l -> avl r ->
  avl (join l x d r) /\
  0<= height (join l x d r) - max (height l) (height r) <= 1.
 Proof.
@@ -344,9 +345,9 @@ Hint Resolve concat_avl.
 
 (** split *)
 
-Lemma split_avl : forall m x, avl m -> 
+Lemma split_avl : forall m x, avl m ->
   avl (split x m)#l /\ avl (split x m)#r.
-Proof. 
+Proof.
  intros m x; functional induction (split x m); simpl; auto.
  rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
  simpl; inversion_clear 1; auto.
@@ -356,12 +357,12 @@ Qed.
 End Elt.
 Hint Constructors avl.
 
-Section Map. 
+Section Map.
 Variable elt elt' : Type.
-Variable f : elt -> elt'. 
+Variable f : elt -> elt'.
 
 Lemma map_height : forall m, height (map f m) = height m.
-Proof. 
+Proof.
 destruct m; simpl; auto.
 Qed.
 
@@ -375,10 +376,10 @@ End Map.
 
 Section Mapi.
 Variable elt elt' : Type.
-Variable f : key -> elt -> elt'. 
+Variable f : key -> elt -> elt'.
 
 Lemma mapi_height : forall m, height (mapi f m) = height m.
-Proof. 
+Proof.
 destruct m; simpl; auto.
 Qed.
 
@@ -390,7 +391,7 @@ Qed.
 
 End Mapi.
 
-Section Map_option. 
+Section Map_option.
 Variable elt elt' : Type.
 Variable f : key -> elt -> option elt'.
 
@@ -412,12 +413,12 @@ Hypothesis mapr_avl : forall m', avl m' -> avl (mapr m').
 
 Notation map2_opt := (map2_opt f mapl mapr).
 
-Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 -> 
+Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 ->
  avl (map2_opt m1 m2).
 Proof.
-intros m1 m2; functional induction (map2_opt m1 m2); auto; 
-factornode _x0 _x1 _x2 _x3 _x4 as r2; intros; 
-destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl; 
+intros m1 m2; functional induction (map2_opt m1 m2); auto;
+factornode _x0 _x1 _x2 _x3 _x4 as r2; intros;
+destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl;
 auto using join_avl, concat_avl.
 Qed.
 
@@ -437,11 +438,11 @@ End AvlProofs.
 
 (** * Encapsulation
 
-   We can implement [S] with balanced binary search trees. 
+   We can implement [S] with balanced binary search trees.
    When compared to [FMapAVL], we maintain here two invariants
    (bst and avl) instead of only bst, which is enough for fulfilling
    the FMap interface.
-*) 
+*)
 
 Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
@@ -450,32 +451,32 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Import Raw.
  Import Raw.Proofs.
 
- Record bbst (elt:Type) := 
+ Record bbst (elt:Type) :=
   Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}.
- 
+
  Definition t := bbst.
  Definition key := E.t.
- 
+
  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 := Bbst (empty_bst elt) (empty_avl elt).
  Definition is_empty m : bool := is_empty m.(this).
- Definition add x e m : t elt := 
+ Definition add x e m : t elt :=
   Bbst (add_bst x e m.(is_bst)) (add_avl x e m.(is_avl)).
- Definition remove x m : t elt := 
+ Definition remove x m : t elt :=
   Bbst (remove_bst x m.(is_bst)) (remove_avl x m.(is_avl)).
  Definition mem x m : bool := mem x m.(this).
  Definition find x m : option elt := find x m.(this).
- Definition map f m : t elt' := 
+ Definition map f m : t elt' :=
   Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
- Definition mapi (f:key->elt->elt') m : t elt' := 
+ Definition mapi (f:key->elt->elt') m : t elt' :=
   Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)).
- Definition map2 f m (m':t elt') : t elt'' := 
+ Definition map2 f m (m':t elt') : t elt'' :=
   Bbst (map2_bst f m.(is_bst) m'.(is_bst)) (map2_avl f m.(is_avl) m'.(is_avl)).
  Definition elements m : list (key*elt) := elements m.(this).
  Definition cardinal m := cardinal m.(this).
@@ -492,14 +493,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.
@@ -530,7 +531,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.
@@ -539,36 +540,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.
@@ -576,23 +577,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,a) (m',b',a') 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,a) (m',b',a') 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,a) (m',b',a') cmp; rewrite Equivb_Equivb; 
+ Proof.
+ unfold equal; intros (m,b,a) (m',b',a') 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.
 
@@ -600,10 +601,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)
@@ -613,10 +614,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).
@@ -624,9 +625,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).
@@ -636,54 +637,54 @@ 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).
   Import AvlProofs.
   Import Raw.Proofs.
   Module Import MD := OrderedTypeFacts(D).
   Module LO := FMapList.Make_ord(X)(D).
 
-  Definition t := MapS.t D.t. 
+  Definition t := MapS.t D.t.
 
-  Definition cmp e e' := 
+  Definition cmp e e' :=
    match D.compare e e' with EQ _ => true | _ => false end.
 
-  Definition elements (m:t) := 
+  Definition elements (m:t) :=
     LO.MapS.Build_slist (Raw.Proofs.elements_sort m.(is_bst)).
 
-  (** * As comparison function, we propose here a non-structural 
-    version faithful to the code of Ocaml's Map library, instead of 
+  (** * As comparison function, we propose here a non-structural
+    version faithful to the code of Ocaml's Map library, instead of
     the structural version of FMapAVL *)
 
-  Fixpoint cardinal_e (e:Raw.enumeration D.t) := 
-    match e with 
+  Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
+    match e with
      | Raw.End => 0%nat
      | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
     end.
 
-  Lemma cons_cardinal_e : forall m e, 
+  Lemma cons_cardinal_e : forall m e,
    cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat.
   Proof.
    induction m; simpl; intros; auto.
    rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith.
   Qed.
 
-  Definition cardinal_e_2 ee := 
+  Definition cardinal_e_2 ee :=
    (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.
 
-  Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) 
-   { measure cardinal_e_2 ee } : comparison := 
-  match ee with 
+  Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
+   { measure cardinal_e_2 ee } : comparison :=
+  match ee with
   | (Raw.End, Raw.End) => Eq
   | (Raw.End, Raw.More _ _ _ _) => Lt
   | (Raw.More _ _ _ _, Raw.End) => Gt
   | (Raw.More x1 d1 r1 e1, Raw.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 _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
                 | LT _ => Lt
                 | GT _ => Gt
@@ -693,10 +694,10 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
       end
   end.
   Proof.
-  intros; unfold cardinal_e_2; simpl; 
+  intros; unfold cardinal_e_2; simpl;
   abstract (do 2 rewrite cons_cardinal_e; romega with * ).
   Defined.
-  
+
   Definition Cmp c :=
    match c with
     | Eq => LO.eq_list
@@ -704,7 +705,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.
@@ -712,23 +713,23 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Qed.
   Hint Resolve cons_Cmp.
 
-  Lemma compare_aux_Cmp : forall e, 
+  Lemma compare_aux_Cmp : forall e,
    Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
   Proof.
-  intros e; functional induction (compare_aux e); simpl in *; 
+  intros e; functional induction (compare_aux e); simpl in *;
    auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto.
   rewrite 2 cons_1 in IHc; auto.
   Qed.
 
-  Lemma compare_Cmp : forall m1 m2, 
-    Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))) 
+  Lemma compare_Cmp : forall m1 m2,
+    Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _)))
      (Raw.elements m1) (Raw.elements m2).
   Proof.
-  intros. 
+  intros.
   assert (H1:=cons_1 m1 (Raw.End _)).
   assert (H2:=cons_1 m2 (Raw.End _)).
   simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2.
-  apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), 
+  apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _),
                            Raw.cons m2 (Raw.End _))).
   Qed.
 
@@ -737,15 +738,15 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
 
   Definition compare (s s':t) : Compare lt eq s s'.
   Proof.
-   intros (s,b,a) (s',b',a').
+   destruct s as (s,b,a), s' as (s',b',a').
    generalize (compare_Cmp s s').
    destruct compare_aux; 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 (elements_sort m1.(is_bst)).
 
   Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
@@ -782,7 +783,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.
 
@@ -799,13 +800,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.
 
@@ -816,8 +817,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).