Updated PR by removing whitespaces. Bug 17450.

1 files changed, 113 insertions, 113 deletions

diff --git a/lib/Maps.v b/lib/Maps.v
index 63ac0c09..39fec9fd 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -126,7 +126,7 @@ Module Type TREE.
     forall (A: Type) (m: t A) (i: elt) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Hypothesis elements_keys_norepet:
-    forall (A: Type) (m: t A), 
+    forall (A: Type) (m: t A),
     list_norepet (List.map (@fst elt A) (elements m)).
   Hypothesis elements_extensional:
     forall (A: Type) (m n: t A),
@@ -396,7 +396,7 @@ Module PTree <: TREE.
       generalize (H xH); simpl; congruence.
       destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1.
       destruct x; simpl; auto.
-      apply andb_true_intro; split. 
+      apply andb_true_intro; split.
       apply IHm1. intros; apply (H (xO x)).
       apply IHm2. intros; apply (H (xI x)).
     Qed.
@@ -414,18 +414,18 @@ Module PTree <: TREE.
       induction m1; intros.
     - simpl. rewrite bempty_correct. split; intros.
       rewrite gleaf. rewrite H. auto.
-      generalize (H x). rewrite gleaf. destruct (get x m2); tauto. 
+      generalize (H x). rewrite gleaf. destruct (get x m2); tauto.
     - destruct m2.
       + unfold beq. rewrite bempty_correct. split; intros.
         rewrite H. rewrite gleaf. auto.
         generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto.
       + simpl. split; intros.
         * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
-          rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. 
+          rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
           destruct x; simpl. apply H1. apply H3.
           destruct o; destruct o0; auto || congruence.
         * apply andb_true_intro. split. apply andb_true_intro. split.
-          generalize (H xH); simpl. destruct o; destruct o0; tauto. 
+          generalize (H xH); simpl. destruct o; destruct o0; tauto.
           apply IHm1_1. intros; apply (H (xO x)).
           apply IHm1_2. intros; apply (H (xI x)).
     Qed.
@@ -450,7 +450,7 @@ Module PTree <: TREE.
     intros j. simpl. rewrite IH. reflexivity.
     intros j. simpl. rewrite IH. reflexivity.
   Qed.
-  
+
   Lemma prev_involutive i :
     prev (prev i) = i.
   Proof (prev_append_prev i xH).
@@ -513,7 +513,7 @@ Module PTree <: TREE.
     forall (A: Type) (l r: t A) (x: option A) (i: positive),
     get i (Node' l x r) = get i (Node l x r).
   Proof.
-    intros. unfold Node'. 
+    intros. unfold Node'.
     destruct l; destruct x; destruct r; auto.
     destruct i; simpl; auto; rewrite gleaf; auto.
   Qed.
@@ -531,9 +531,9 @@ Module PTree <: TREE.
     get i (filter1 pred m) =
     match get i m with None => None | Some x => if pred x then Some x else None end.
   Proof.
-    intros until m. revert m i. induction m; simpl; intros. 
+    intros until m. revert m i. induction m; simpl; intros.
     rewrite gleaf; auto.
-    rewrite gnode'. destruct i; simpl; auto. destruct o; auto. 
+    rewrite gnode'. destruct i; simpl; auto. destruct o; auto.
   Qed.
 
   Section COMBINE.
@@ -589,7 +589,7 @@ Module PTree <: TREE.
     induction m1; intros; simpl.
     rewrite gleaf. apply xgcombine_r.
     destruct m2; simpl.
-    rewrite gleaf. rewrite <- xgcombine_l. auto. 
+    rewrite gleaf. rewrite <- xgcombine_l. auto.
     repeat rewrite gnode'. destruct i; simpl; auto.
   Qed.
 
@@ -622,10 +622,10 @@ Module PTree <: TREE.
       auto.
      rewrite IHm1_1.
      rewrite IHm1_2.
-     auto. 
+     auto.
   Qed.
 
-    Fixpoint xelements (A : Type) (m : t A) (i : positive) 
+    Fixpoint xelements (A : Type) (m : t A) (i : positive)
                        (k: list (positive * A)) {struct m}
                        : list (positive * A) :=
       match m with
@@ -651,7 +651,7 @@ Module PTree <: TREE.
   Remark xelements_leaf:
     forall A i, xelements (@Leaf A) i nil = nil.
   Proof.
-    intros; reflexivity. 
+    intros; reflexivity.
   Qed.
 
   Remark xelements_node:
@@ -685,8 +685,8 @@ Module PTree <: TREE.
         apply xelements_incl. right. auto.
         auto.
         inv H. apply xelements_incl. left. reflexivity.
-        apply xelements_incl. auto. 
-        auto. 
+        apply xelements_incl. auto.
+        auto.
         inv H.
     Qed.
 
@@ -694,7 +694,7 @@ Module PTree <: TREE.
     forall (A: Type) (m: t A) (i: positive) (v: A),
     get i m = Some v -> In (i, v) (elements m).
   Proof.
-    intros A m i v H. 
+    intros A m i v H.
     generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id.
   Qed.
 
@@ -703,11 +703,11 @@ Module PTree <: TREE.
     In (k, v) (xelements m i nil) ->
     exists j, k = prev (prev_append j i) /\ get j m = Some v.
   Proof.
-    induction m; intros. 
+    induction m; intros.
   - rewrite xelements_leaf in H. contradiction.
   - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]].
     + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); auto.
-    + destruct o; simpl in P; intuition auto. inv H. exists xH; auto. 
+    + destruct o; simpl in P; intuition auto. inv H. exists xH; auto.
     + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); auto.
   Qed.
 
@@ -715,8 +715,8 @@ Module PTree <: TREE.
     forall (A: Type) (m: t A) (i: positive) (v: A),
     In (i, v) (elements m) -> get i m = Some v.
   Proof.
-    unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). 
-    rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. 
+    unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q).
+    rewrite prev_append_prev in P. change i with (prev_append 1 i) in P.
     exploit prev_append_inj; eauto. intros; congruence.
   Qed.
 
@@ -726,7 +726,7 @@ Module PTree <: TREE.
   Remark xkeys_leaf:
     forall A i, xkeys (@Leaf A) i = nil.
   Proof.
-    intros; reflexivity. 
+    intros; reflexivity.
   Qed.
 
   Remark xkeys_node:
@@ -736,7 +736,7 @@ Module PTree <: TREE.
     ++ match o with None => nil | Some v => prev i :: nil end
     ++ xkeys m2 (xI i).
   Proof.
-    intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto. 
+    intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto.
   Qed.
 
   Lemma in_xkeys:
@@ -746,7 +746,7 @@ Module PTree <: TREE.
   Proof.
     unfold xkeys; intros.
     apply (list_in_map_inv) in H. destruct H as ((j, v) & -> & H).
-    exploit in_xelements; eauto. intros (k & P & Q). exists k; auto. 
+    exploit in_xelements; eauto. intros (k & P & Q). exists k; auto.
   Qed.
 
   Lemma xelements_keys_norepet:
@@ -756,26 +756,26 @@ Module PTree <: TREE.
     induction m; intros.
   - rewrite xkeys_leaf; constructor.
   - assert (NOTIN1: ~ In (prev i) (xkeys m1 (xO i))).
-    { red; intros. exploit in_xkeys; eauto. intros (j & EQ). 
+    { red; intros. exploit in_xkeys; eauto. intros (j & EQ).
       rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. }
     assert (NOTIN2: ~ In (prev i) (xkeys m2 (xI i))).
-    { red; intros. exploit in_xkeys; eauto. intros (j & EQ). 
+    { red; intros. exploit in_xkeys; eauto. intros (j & EQ).
       rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. }
     assert (DISJ: forall x, In x (xkeys m1 (xO i)) -> In x (xkeys m2 (xI i)) -> False).
-    { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1). 
-      exploit in_xkeys. eexact H0. intros (j2 & EQ2). 
+    { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1).
+      exploit in_xkeys. eexact H0. intros (j2 & EQ2).
       rewrite prev_append_prev in *. simpl in *. rewrite EQ2 in EQ1. apply prev_append_inj in EQ1. discriminate. }
-    rewrite xkeys_node. apply list_norepet_append. auto. 
+    rewrite xkeys_node. apply list_norepet_append. auto.
     destruct o; simpl; auto. constructor; auto.
-    red; intros. red; intros; subst y. destruct o; simpl in H0. 
-    destruct H0. subst x. tauto. eauto. eauto. 
+    red; intros. red; intros; subst y. destruct o; simpl in H0.
+    destruct H0. subst x. tauto. eauto. eauto.
   Qed.
 
   Theorem elements_keys_norepet:
-    forall (A: Type) (m: t A), 
+    forall (A: Type) (m: t A),
     list_norepet (List.map (@fst elt A) (elements m)).
   Proof.
-    intros. apply (xelements_keys_norepet m xH). 
+    intros. apply (xelements_keys_norepet m xH).
   Qed.
 
   Remark xelements_empty:
@@ -783,7 +783,7 @@ Module PTree <: TREE.
   Proof.
     induction m; intros.
     auto.
-    rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. 
+    rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto.
     generalize (H xH); simpl; congruence.
     intros. apply (H (xI i0)).
     intros. apply (H (xO i0)).
@@ -806,29 +806,29 @@ Module PTree <: TREE.
       (xelements m j nil) (xelements n j nil)).
   {
     induction m; intros.
-  - rewrite xelements_leaf. rewrite xelements_empty. constructor. 
-    intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. 
+  - rewrite xelements_leaf. rewrite xelements_empty. constructor.
+    intros. destruct (get i n) eqn:E; auto. exploit H0; eauto.
     intros [x [P Q]]. rewrite gleaf in P; congruence.
-  - destruct n as [ | n1 o' n2 ]. 
+  - destruct n as [ | n1 o' n2 ].
     + rewrite xelements_leaf, xelements_empty. constructor.
-      intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto. 
+      intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto.
       intros [x [P Q]]. rewrite gleaf in P; congruence.
     + rewrite ! xelements_node. apply list_forall2_app.
-      apply IHm1. 
-      intros. apply (H (xO i) x); auto. 
+      apply IHm1.
+      intros. apply (H (xO i) x); auto.
       intros. apply (H0 (xO i) y); auto.
-      apply list_forall2_app. 
+      apply list_forall2_app.
       destruct o, o'.
-      destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. 
+      destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P.
       constructor. auto. constructor.
       destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P.
       destruct (H0 xH b) as [x [P Q]]. auto. simpl in P. inv P.
       constructor.
-      apply IHm2. 
-      intros. apply (H (xI i) x); auto. 
+      apply IHm2.
+      intros. apply (H (xI i) x); auto.
       intros. apply (H0 (xI i) y); auto.
     }
-    intros. apply H with (j := xH); auto. 
+    intros. apply H with (j := xH); auto.
   Qed.
 
   Theorem elements_extensional:
@@ -836,8 +836,8 @@ Module PTree <: TREE.
     (forall i, get i m = get i n) ->
     elements m = elements n.
   Proof.
-    intros. 
-    exploit (elements_canonical_order (fun (x y: A) => x = y) m n). 
+    intros.
+    exploit (elements_canonical_order (fun (x y: A) => x = y) m n).
     intros. rewrite H in H0. exists x; auto.
     intros. rewrite <- H in H0. exists y; auto.
     induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *.
@@ -862,8 +862,8 @@ Module PTree <: TREE.
     {
       destruct i; simpl remove.
       destruct m1; auto. destruct o; auto. destruct (remove i m2); auto.
-      destruct o; auto. destruct m2; auto. destruct (remove i m1); auto. 
-      destruct m1; auto. destruct m2; auto. 
+      destruct o; auto. destruct m2; auto. destruct (remove i m1); auto.
+      destruct m1; auto. destruct m2; auto.
     }
     rewrite REMOVE. destruct i; simpl in H.
     + destruct (IHm2 i (xI j) H) as (l1 & l2 & EQ & EQ').
@@ -883,7 +883,7 @@ Module PTree <: TREE.
       rewrite xelements_node, EQ', ! app_ass. auto.
     + subst o. exists (xelements m1 (xO j) nil); exists (xelements m2 (xI j) nil); split.
       rewrite xelements_node. rewrite prev_append_prev. auto.
-      rewrite xelements_node; auto. 
+      rewrite xelements_node; auto.
   Qed.
 
   Theorem elements_remove:
@@ -891,8 +891,8 @@ Module PTree <: TREE.
     get i m = Some v ->
     exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2.
   Proof.
-    intros. exploit xelements_remove. eauto. instantiate (1 := xH). 
-    rewrite prev_append_prev. auto. 
+    intros. exploit xelements_remove. eauto. instantiate (1 := xH).
+    rewrite prev_append_prev. auto.
   Qed.
 
   Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B)
@@ -920,7 +920,7 @@ Module PTree <: TREE.
     simpl. auto.
     destruct o; simpl.
     rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
-    rewrite <- IHm1. rewrite <- IHm2. auto. 
+    rewrite <- IHm1. rewrite <- IHm2. auto.
   Qed.
 
   Theorem fold_spec:
@@ -928,7 +928,7 @@ Module PTree <: TREE.
     fold f m v =
     List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
   Proof.
-    intros. unfold fold, elements. rewrite <- xfold_xelements. auto. 
+    intros. unfold fold, elements. rewrite <- xfold_xelements. auto.
   Qed.
 
   Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B :=
@@ -952,7 +952,7 @@ Module PTree <: TREE.
     simpl. auto.
     destruct o; simpl.
     rewrite <- IHm1. simpl. rewrite <- IHm2. auto.
-    rewrite <- IHm1. rewrite <- IHm2. auto. 
+    rewrite <- IHm1. rewrite <- IHm2. auto.
   Qed.
 
   Theorem fold1_spec:
@@ -960,7 +960,7 @@ Module PTree <: TREE.
     fold1 f m v =
     List.fold_left (fun a p => f a (snd p)) (elements m) v.
   Proof.
-    intros. apply fold1_xelements with (l := @nil (positive * A)). 
+    intros. apply fold1_xelements with (l := @nil (positive * A)).
   Qed.
 
 End PTree.
@@ -1064,7 +1064,7 @@ Module IMap(X: INDEXED_TYPE).
   Lemma gi:
     forall (A: Type) (x: A) (i: X.t), get i (init x) = x.
   Proof.
-    intros. unfold get, init. apply PMap.gi. 
+    intros. unfold get, init. apply PMap.gi.
   Qed.
 
   Lemma gss:
@@ -1077,19 +1077,19 @@ Module IMap(X: INDEXED_TYPE).
     forall (A: Type) (i j: X.t) (x: A) (m: t A),
     i <> j -> get i (set j x m) = get i m.
   Proof.
-    intros. unfold get, set. apply PMap.gso. 
-    red. intro. apply H. apply X.index_inj; auto. 
+    intros. unfold get, set. apply PMap.gso.
+    red. intro. apply H. apply X.index_inj; auto.
   Qed.
 
   Lemma gsspec:
     forall (A: Type) (i j: X.t) (x: A) (m: t A),
     get i (set j x m) = if X.eq i j then x else get i m.
   Proof.
-    intros. unfold get, set. 
+    intros. unfold get, set.
     rewrite PMap.gsspec.
     case (X.eq i j); intro.
     subst j. rewrite peq_true. reflexivity.
-    rewrite peq_false. reflexivity. 
+    rewrite peq_false. reflexivity.
     red; intro. elim n. apply X.index_inj; auto.
   Qed.
 
@@ -1097,7 +1097,7 @@ Module IMap(X: INDEXED_TYPE).
     forall (A B: Type) (f: A -> B) (i: X.t) (m: t A),
     get i (map f m) = f(get i m).
   Proof.
-    intros. unfold map, get. apply PMap.gmap. 
+    intros. unfold map, get. apply PMap.gmap.
   Qed.
 
   Lemma set2:
@@ -1225,7 +1225,7 @@ Hypothesis P_compat:
   (forall x, T.get x m = T.get x m') ->
   P m a -> P m' a.
 
-Hypothesis H_base: 
+Hypothesis H_base:
   P (T.empty _) init.
 
 Hypothesis H_rec:
@@ -1253,23 +1253,23 @@ Remark H_rec':
   P' l a ->
   P' (l ++ (k, v) :: nil) (f a k v).
 Proof.
-  unfold P'; intros.  
-  set (m0 := T.remove k m). 
+  unfold P'; intros.
+  set (m0 := T.remove k m).
   apply P_compat with (T.set k v m0).
     intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k).
     symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)).
     apply in_or_app. simpl. intuition congruence.
     apply T.gro. auto.
-  apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. 
-  apply H1. red. intros [k' v']. 
-  split; intros. 
-  apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. 
-  rewrite <- (H2 (k', v')). apply in_or_app. auto. 
+  apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto.
+  apply H1. red. intros [k' v'].
+  split; intros.
+  apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete.
+  rewrite <- (H2 (k', v')). apply in_or_app. auto.
   red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto.
   assert (T.get k' m0 = Some v'). apply T.elements_complete. auto.
   unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence.
   assert (In (k', v') (T.elements m)). apply T.elements_correct; auto.
-  rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. 
+  rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto.
   simpl in H6. intuition congruence.
 Qed.
 
@@ -1282,10 +1282,10 @@ Lemma fold_rec_aux:
 Proof.
   induction l1; intros; simpl.
   rewrite <- List.app_nil_end. auto.
-  destruct a as [k v]; simpl in *. inv H1. 
+  destruct a as [k v]; simpl in *. inv H1.
   change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1.
   rewrite app_ass. auto.
-  red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. 
+  red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib.
   simpl in H4. intuition congruence.
   auto.
   unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib.
@@ -1300,8 +1300,8 @@ Proof.
     apply fold_rec_aux.
     simpl. red; intros; tauto.
     simpl. red; intros. elim H0.
-    apply T.elements_keys_norepet. 
-    apply H_base'. 
+    apply T.elements_keys_norepet.
+    apply H_base'.
   simpl in H. red in H. apply H. red; intros. tauto.
 Qed.
 
@@ -1319,18 +1319,18 @@ Theorem cardinal_remove:
   forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat.
 Proof.
   unfold cardinal; intros.
-  exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). 
+  exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q).
   rewrite P, Q. rewrite ! app_length. simpl. omega.
 Qed.
 
 Theorem cardinal_set:
   forall x m y, T.get x m = None -> (cardinal m < cardinal (T.set x y m))%nat.
 Proof.
-  intros. set (m' := T.set x y m). 
-  replace (cardinal m) with (cardinal (T.remove x m')). 
-  apply cardinal_remove with y. unfold m'; apply T.gss. 
-  unfold cardinal. f_equal. apply T.elements_extensional. 
-  intros. unfold m'. rewrite T.grspec, T.gsspec. 
+  intros. set (m' := T.set x y m).
+  replace (cardinal m) with (cardinal (T.remove x m')).
+  apply cardinal_remove with y. unfold m'; apply T.gss.
+  unfold cardinal. f_equal. apply T.elements_extensional.
+  intros. unfold m'. rewrite T.grspec, T.gsspec.
   destruct (T.elt_eq i x); auto. congruence.
 Qed.
 
@@ -1352,16 +1352,16 @@ Proof.
   intros m0 f.
   unfold for_all. apply fold_rec; intros.
 - (* Extensionality *)
-  rewrite H0. split; intros. rewrite <- H in H2; auto. rewrite H in H2; auto. 
+  rewrite H0. split; intros. rewrite <- H in H2; auto. rewrite H in H2; auto.
 - (* Base case *)
   split; intros. rewrite T.gempty in H0; congruence. auto.
 - (* Inductive case *)
   split; intros.
-  destruct (andb_prop _ _ H2). rewrite T.gsspec in H3. destruct (T.elt_eq x k). 
+  destruct (andb_prop _ _ H2). rewrite T.gsspec in H3. destruct (T.elt_eq x k).
   inv H3. auto.
   apply H1; auto.
-  apply andb_true_intro. split. 
-  rewrite H1. intros. apply H2. rewrite T.gso; auto. congruence. 
+  apply andb_true_intro. split.
+  rewrite H1. intros. apply H2. rewrite T.gso; auto. congruence.
   apply H2. apply T.gss.
 Qed.
 
@@ -1375,7 +1375,7 @@ Proof.
   intros m0 f.
   unfold exists_. apply fold_rec; intros.
 - (* Extensionality *)
-  rewrite H0. split; intros (x0 & a0 & P & Q); exists x0; exists a0; split; auto; congruence. 
+  rewrite H0. split; intros (x0 & a0 & P & Q); exists x0; exists a0; split; auto; congruence.
 - (* Base case *)
   split; intros. congruence. destruct H as (x & a & P & Q). rewrite T.gempty in P; congruence.
 - (* Inductive case *)
@@ -1383,7 +1383,7 @@ Proof.
   destruct (orb_true_elim _ _ H2).
   rewrite H1 in e. destruct e as (x1 & a1 & P & Q).
   exists x1; exists a1; split; auto. rewrite T.gso; auto. congruence.
-  exists k; exists v; split; auto. apply T.gss. 
+  exists k; exists v; split; auto. apply T.gss.
   destruct H2 as (x1 & a1 & P & Q). apply orb_true_intro.
   rewrite T.gsspec in P. destruct (T.elt_eq x1 k).
   inv P. right; auto.
@@ -1394,11 +1394,11 @@ Remark exists_for_all:
   forall m f,
   exists_ m f = negb (for_all m (fun x a => negb (f x a))).
 Proof.
-  intros. unfold exists_, for_all. rewrite ! T.fold_spec. 
-  change false with (negb true). generalize (T.elements m) true. 
+  intros. unfold exists_, for_all. rewrite ! T.fold_spec.
+  change false with (negb true). generalize (T.elements m) true.
   induction l; simpl; intros.
   auto.
-  rewrite <- IHl. f_equal. 
+  rewrite <- IHl. f_equal.
   destruct b; destruct (f (fst a) (snd a)); reflexivity.
 Qed.
 
@@ -1406,11 +1406,11 @@ Remark for_all_exists:
   forall m f,
   for_all m f = negb (exists_ m (fun x a => negb (f x a))).
 Proof.
-  intros. unfold exists_, for_all. rewrite ! T.fold_spec. 
-  change true with (negb false). generalize (T.elements m) false. 
+  intros. unfold exists_, for_all. rewrite ! T.fold_spec.
+  change true with (negb false). generalize (T.elements m) false.
   induction l; simpl; intros.
   auto.
-  rewrite <- IHl. f_equal. 
+  rewrite <- IHl. f_equal.
   destruct b; destruct (f (fst a) (snd a)); reflexivity.
 Qed.
 
@@ -1418,20 +1418,20 @@ Lemma for_all_false:
   forall m f,
   for_all m f = false <-> (exists x a, T.get x m = Some a /\ f x a = false).
 Proof.
-  intros. rewrite for_all_exists. 
-  rewrite negb_false_iff. rewrite exists_correct. 
-  split; intros (x & a & P & Q); exists x; exists a; split; auto. 
+  intros. rewrite for_all_exists.
+  rewrite negb_false_iff. rewrite exists_correct.
+  split; intros (x & a & P & Q); exists x; exists a; split; auto.
   rewrite negb_true_iff in Q. auto.
-  rewrite Q; auto. 
+  rewrite Q; auto.
 Qed.
 
 Lemma exists_false:
   forall m f,
   exists_ m f = false <-> (forall x a, T.get x m = Some a -> f x a = false).
 Proof.
-  intros. rewrite exists_for_all. 
+  intros. rewrite exists_for_all.
   rewrite negb_false_iff. rewrite for_all_correct.
-  split; intros. apply H in H0. rewrite negb_true_iff in H0. auto. rewrite H; auto. 
+  split; intros. apply H in H0. rewrite negb_true_iff in H0. auto. rewrite H; auto.
 Qed.
 
 End FORALL_EXISTS.
@@ -1457,20 +1457,20 @@ Proof.
   set (p1 := fun x a1 => match T.get x m2 with None => false | Some a2 => beqA a1 a2 end).
   set (p2 := fun x a2 => match T.get x m1 with None => false | Some a1 => beqA a1 a2 end).
   destruct (for_all m1 p1) eqn:F1; [destruct (for_all m2 p2) eqn:F2 | idtac].
-  + cut (T.beq beqA m1 m2 = true). congruence. 
-    rewrite for_all_correct in *. rewrite T.beq_correct; intros. 
-    destruct (T.get x m1) as [a1|] eqn:X1. 
+  + cut (T.beq beqA m1 m2 = true). congruence.
+    rewrite for_all_correct in *. rewrite T.beq_correct; intros.
+    destruct (T.get x m1) as [a1|] eqn:X1.
     generalize (F1 _ _ X1). unfold p1. destruct (T.get x m2); congruence.
     destruct (T.get x m2) as [a2|] eqn:X2; auto.
-    generalize (F2 _ _ X2). unfold p2. rewrite X1. congruence. 
+    generalize (F2 _ _ X2). unfold p2. rewrite X1. congruence.
   + rewrite for_all_false in F2. destruct F2 as (x & a & P & Q).
-    exists x. rewrite P. unfold p2 in Q. destruct (T.get x m1); auto. 
+    exists x. rewrite P. unfold p2 in Q. destruct (T.get x m1); auto.
   + rewrite for_all_false in F1. destruct F1 as (x & a & P & Q).
     exists x. rewrite P. unfold p1 in Q. destruct (T.get x m2); auto.
 - (* existence -> beq = false *)
   destruct H as [x P].
-  destruct (T.beq beqA m1 m2) eqn:E; auto. 
-  rewrite T.beq_correct in E. 
+  destruct (T.beq beqA m1 m2) eqn:E; auto.
+  rewrite T.beq_correct in E.
   generalize (E x). destruct (T.get x m1); destruct (T.get x m2); tauto || congruence.
 Qed.
 
@@ -1493,7 +1493,7 @@ Definition Equal (m1 m2: T.t A) : Prop :=
 
 Lemma Equal_refl: forall m, Equal m m.
 Proof.
-  intros; red; intros. destruct (T.get x m); auto. reflexivity. 
+  intros; red; intros. destruct (T.get x m); auto. reflexivity.
 Qed.
 
 Lemma Equal_sym: forall m1 m2, Equal m1 m2 -> Equal m2 m1.
@@ -1505,7 +1505,7 @@ Lemma Equal_trans: forall m1 m2 m3, Equal m1 m2 -> Equal m2 m3 -> Equal m1 m3.
 Proof.
   intros; red; intros. generalize (H x) (H0 x).
   destruct (T.get x m1); destruct (T.get x m2); try tauto;
-  destruct (T.get x m3); try tauto. 
+  destruct (T.get x m3); try tauto.
   intros. transitivity a0; auto.
 Qed.
 
@@ -1525,15 +1525,15 @@ Program Definition Equal_dec (m1 m2: T.t A) : { m1 === m2 } + { m1 =/= m2 } :=
 Next Obligation.
   rename Heq_anonymous into B.
   symmetry in B. rewrite T.beq_correct in B.
-  red; intros. generalize (B x). 
-  destruct (T.get x m1); destruct (T.get x m2); auto. 
-  intros. eapply proj_sumbool_true; eauto. 
+  red; intros. generalize (B x).
+  destruct (T.get x m1); destruct (T.get x m2); auto.
+  intros. eapply proj_sumbool_true; eauto.
 Qed.
 Next Obligation.
   assert (T.beq (fun a1 a2 => proj_sumbool (a1 == a2)) m1 m2 = true).
-  apply T.beq_correct; intros. 
-  generalize (H x). 
-  destruct (T.get x m1); destruct (T.get x m2); try tauto. 
+  apply T.beq_correct; intros.
+  generalize (H x).
+  destruct (T.get x m1); destruct (T.get x m2); try tauto.
   intros. apply proj_sumbool_is_true; auto.
   unfold equiv, complement in H0. congruence.
 Qed.