Updated PR by removing whitespaces. Bug 17450.

1 files changed, 56 insertions, 56 deletions

diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 46a886ea..76dd6b31 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -90,7 +90,7 @@ Module Type UNIONFIND.
   Hypothesis sameclass_union_3:
     forall uf a b x y,
     sameclass (union uf a b) x y ->
-       sameclass uf x y 
+       sameclass uf x y
     \/ sameclass uf x a /\ sameclass uf y b
     \/ sameclass uf x b /\ sameclass uf y a.
 
@@ -120,7 +120,7 @@ Module Type UNIONFIND.
     pathlen (merge uf a b) x =
       if elt_eq (repr uf a) (repr uf b) then
         pathlen uf x
-      else if elt_eq (repr uf x) (repr uf a) then 
+      else if elt_eq (repr uf x) (repr uf a) then
         pathlen uf x + pathlen uf b + 1
       else
         pathlen uf x.
@@ -155,7 +155,7 @@ Definition t := unionfind.
 
 Definition getlink (m: M.t elt) (a: elt) : {a' | M.get a m = Some a'} + {M.get a m = None}.
 Proof.
-  destruct (M.get a m). left. exists e; auto. right; auto. 
+  destruct (M.get a m). left. exists e; auto. right; auto.
 Defined.
 
 (* The canonical representative of an element *)
@@ -175,11 +175,11 @@ Definition repr (a: elt) : elt := Fix uf.(mwf) (fun _ => elt) F_repr a.
 Lemma repr_unroll:
   forall a, repr a = match M.get a uf.(m) with Some a' => repr a' | None => a end.
 Proof.
-  intros. unfold repr at 1. rewrite Fix_eq. 
-  unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q]. 
+  intros. unfold repr at 1. rewrite Fix_eq.
+  unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q].
   rewrite P; auto.
   rewrite Q; auto.
-  intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. 
+  intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto.
 Qed.
 
 Lemma repr_none:
@@ -187,36 +187,36 @@ Lemma repr_none:
   M.get a uf.(m) = None ->
   repr a = a.
 Proof.
-  intros. rewrite repr_unroll. rewrite H; auto. 
+  intros. rewrite repr_unroll. rewrite H; auto.
 Qed.
 
 Lemma repr_some:
-  forall a a', 
+  forall a a',
   M.get a uf.(m) = Some a' ->
   repr a = repr a'.
 Proof.
-  intros. rewrite repr_unroll. rewrite H; auto. 
+  intros. rewrite repr_unroll. rewrite H; auto.
 Qed.
 
 Lemma repr_res_none:
   forall (a: elt), M.get (repr a) uf.(m) = None.
 Proof.
-  apply (well_founded_ind (mwf uf)). intros. 
+  apply (well_founded_ind (mwf uf)). intros.
   rewrite repr_unroll. destruct (M.get x (m uf)) as [y|] eqn:X; auto.
 Qed.
 
 Lemma repr_canonical:
   forall (a: elt), repr (repr a) = repr a.
 Proof.
-  intros. apply repr_none. apply repr_res_none. 
+  intros. apply repr_none. apply repr_res_none.
 Qed.
 
 Lemma repr_some_diff:
   forall a a', M.get a uf.(m) = Some a' -> a <> repr a'.
 Proof.
-  intros; red; intros. 
-  assert (repr a = a). rewrite (repr_some a a'); auto. 
-  assert (M.get a uf.(m) = None). rewrite <- H1. apply repr_res_none. 
+  intros; red; intros.
+  assert (repr a = a). rewrite (repr_some a a'); auto.
+  assert (M.get a uf.(m) = None). rewrite <- H1. apply repr_res_none.
   congruence.
 Qed.
 
@@ -297,9 +297,9 @@ Remark identify_Acc_b:
 Proof.
   induction 1; intros. constructor; intros.
   rewrite identify_order in H2. destruct H2 as [A | [A B]].
-  apply H0; auto. rewrite <- (repr_some uf _ _ A). auto. 
+  apply H0; auto. rewrite <- (repr_some uf _ _ A). auto.
   subst. elim H1. apply repr_none. auto.
-Qed.  
+Qed.
 
 Remark identify_Acc:
   forall x,
@@ -308,13 +308,13 @@ Proof.
   induction 1. constructor; intros.
   rewrite identify_order in H1. destruct H1 as [A | [A B]].
   auto.
-  subst. apply identify_Acc_b; auto. apply uf.(mwf). 
+  subst. apply identify_Acc_b; auto. apply uf.(mwf).
 Qed.
 
 Lemma identify_wf:
   well_founded (order (M.set a b uf.(m))).
 Proof.
-  red; intros. apply identify_Acc. apply uf.(mwf). 
+  red; intros. apply identify_Acc. apply uf.(mwf).
 Qed.
 
 Definition identify := mk (M.set a b uf.(m)) identify_wf.
@@ -323,11 +323,11 @@ Lemma repr_identify_1:
   forall x, repr uf x <> a -> repr identify x = repr uf x.
 Proof.
   intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
-  rewrite (repr_unroll uf) in *. 
+  rewrite (repr_unroll uf) in *.
   destruct (M.get x (m uf)) as [a'|] eqn:X.
   rewrite <- H; auto.
   apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
-  apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto.  
+  apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto.
 Qed.
 
 Lemma repr_identify_2:
@@ -335,9 +335,9 @@ Lemma repr_identify_2:
 Proof.
   intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
   rewrite (repr_unroll uf) in H0. destruct (M.get x (m uf)) as [a'|] eqn:X.
-  rewrite <- (H a'); auto. 
+  rewrite <- (H a'); auto.
   apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
-  subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec. 
+  subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec.
   rewrite dec_eq_true. apply repr_identify_1. auto.
 Qed.
 
@@ -348,7 +348,7 @@ End IDENTIFY.
 Remark union_not_same_class:
   forall uf a b, repr uf a <> repr uf b -> repr uf (repr uf b) <> repr uf a.
 Proof.
-  intros. rewrite repr_canonical. auto. 
+  intros. rewrite repr_canonical. auto.
 Qed.
 
 Definition union (uf: t) (a b: elt) : t :=
@@ -402,7 +402,7 @@ Qed.
 Lemma sameclass_union_3:
   forall uf a b x y,
   sameclass (union uf a b) x y ->
-     sameclass uf x y 
+     sameclass uf x y
   \/ sameclass uf x a /\ sameclass uf y b
   \/ sameclass uf x b /\ sameclass uf y a.
 Proof.
@@ -448,14 +448,14 @@ Definition path_ord (uf: t) : elt -> elt -> Prop := order uf.(m).
 Lemma path_ord_wellfounded:
   forall uf, well_founded (path_ord uf).
 Proof.
-  intros. apply mwf. 
+  intros. apply mwf.
 Qed.
 
 Lemma path_ord_canonical:
   forall uf x y, repr uf x = x -> ~path_ord uf y x.
 Proof.
   intros; red; intros. hnf in H0.
-  assert (M.get x (m uf) = None). rewrite <- H. apply repr_res_none. 
+  assert (M.get x (m uf) = None). rewrite <- H. apply repr_res_none.
   congruence.
 Qed.
 
@@ -463,10 +463,10 @@ Lemma path_ord_merge_1:
   forall uf a b x y,
   path_ord uf x y -> path_ord (merge uf a b) x y.
 Proof.
-  intros. unfold merge. 
+  intros. unfold merge.
   destruct (M.elt_eq (repr uf a) (repr uf b)).
   auto.
-  red. simpl. red. rewrite M.gsspec. rewrite dec_eq_false. apply H. 
+  red. simpl. red. rewrite M.gsspec. rewrite dec_eq_false. apply H.
   red; intros. hnf in H. generalize (repr_res_none uf a). congruence.
 Qed.
 
@@ -497,11 +497,11 @@ Definition pathlen (a: elt) : nat := Fix uf.(mwf) (fun _ => nat) F_pathlen a.
 Lemma pathlen_unroll:
   forall a, pathlen a = match M.get a uf.(m) with Some a' => S(pathlen a') | None => O end.
 Proof.
-  intros. unfold pathlen at 1. rewrite Fix_eq. 
-  unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q]. 
+  intros. unfold pathlen at 1. rewrite Fix_eq.
+  unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q].
   rewrite P; auto.
   rewrite Q; auto.
-  intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. 
+  intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto.
 Qed.
 
 Lemma pathlen_none:
@@ -509,11 +509,11 @@ Lemma pathlen_none:
   M.get a uf.(m) = None ->
   pathlen a = 0.
 Proof.
-  intros. rewrite pathlen_unroll. rewrite H; auto. 
+  intros. rewrite pathlen_unroll. rewrite H; auto.
 Qed.
 
 Lemma pathlen_some:
-  forall a a', 
+  forall a a',
   M.get a uf.(m) = Some a' ->
   pathlen a = S (pathlen a').
 Proof.
@@ -524,8 +524,8 @@ Lemma pathlen_zero:
   forall a, repr uf a = a <-> pathlen a = O.
 Proof.
   intros; split; intros.
-  apply pathlen_none. rewrite <- H. apply repr_res_none. 
-  apply repr_none. rewrite pathlen_unroll in H. 
+  apply pathlen_none. rewrite <- H. apply repr_res_none.
+  apply repr_none. rewrite pathlen_unroll in H.
   destruct (M.get a (m uf)); congruence.
 Qed.
 
@@ -538,27 +538,27 @@ Lemma pathlen_merge:
   pathlen (merge uf a b) x =
     if M.elt_eq (repr uf a) (repr uf b) then
       pathlen uf x
-    else if M.elt_eq (repr uf x) (repr uf a) then 
+    else if M.elt_eq (repr uf x) (repr uf a) then
       pathlen uf x + pathlen uf b + 1
     else
       pathlen uf x.
 Proof.
-  intros. unfold merge. 
+  intros. unfold merge.
   destruct (M.elt_eq (repr uf a) (repr uf b)).
   auto.
   set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)).
   pattern x. apply (well_founded_ind (mwf uf')); intros.
   rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G.
-  rewrite H; auto. simpl in G. rewrite M.gsspec in G. 
+  rewrite H; auto. simpl in G. rewrite M.gsspec in G.
   destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true.
-  inversion G. subst x'. rewrite dec_eq_false; auto. 
-  replace (pathlen uf (repr uf a)) with 0. omega. 
-  symmetry. apply pathlen_none. apply repr_res_none. 
+  inversion G. subst x'. rewrite dec_eq_false; auto.
+  replace (pathlen uf (repr uf a)) with 0. omega.
+  symmetry. apply pathlen_none. apply repr_res_none.
   rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G.
-  destruct (M.elt_eq (repr uf x') (repr uf a)); omega. 
+  destruct (M.elt_eq (repr uf x') (repr uf a)); omega.
   simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate.
-  rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. 
-  symmetry. apply pathlen_zero; auto. apply repr_none; auto. 
+  rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto.
+  symmetry. apply pathlen_zero; auto. apply repr_none; auto.
 Qed.
 
 Lemma pathlen_gt_merge:
@@ -567,7 +567,7 @@ Lemma pathlen_gt_merge:
   pathlen uf x > pathlen uf y ->
   pathlen (merge uf a b) x > pathlen (merge uf a b) y.
 Proof.
-  intros. repeat rewrite pathlen_merge. 
+  intros. repeat rewrite pathlen_merge.
   destruct (M.elt_eq (repr uf a) (repr uf b)). auto.
   rewrite H. destruct (M.elt_eq (repr uf y) (repr uf a)).
   omega. auto.
@@ -600,7 +600,7 @@ Proof.
   induction 1. constructor; intros.
   destruct (compress_order _ _ H1) as [A | [A B]].
   auto.
-  subst x y. constructor; intros. 
+  subst x y. constructor; intros.
   destruct (compress_order _ _ H2) as [A | [A B]].
   red in A. generalize (repr_res_none uf a). congruence.
   congruence.
@@ -609,7 +609,7 @@ Qed.
 Lemma compress_wf:
   well_founded (order (M.set a b uf.(m))).
 Proof.
-  red; intros. apply compress_Acc. apply uf.(mwf). 
+  red; intros. apply compress_Acc. apply uf.(mwf).
 Qed.
 
 Definition compress := mk (M.set a b uf.(m)) compress_wf.
@@ -620,11 +620,11 @@ Proof.
   apply (well_founded_ind (mwf compress)); intros.
   rewrite (repr_unroll compress).
   destruct (M.get x (m compress)) as [y|] eqn:G.
-  rewrite H; auto. 
-  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). 
+  rewrite H; auto.
+  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a).
   inversion G. subst x y. rewrite <- a_repr_b. apply repr_canonical.
   symmetry; apply repr_some; auto.
-  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). 
+  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a).
   congruence.
   symmetry; apply repr_none; auto.
 Qed.
@@ -637,7 +637,7 @@ Section FIND.
 
 Variable uf: t.
 
-Program Fixpoint find_x (a: elt) {wf (order uf.(m)) a} : 
+Program Fixpoint find_x (a: elt) {wf (order uf.(m)) a} :
     { r: elt * t | fst r = repr uf a /\ forall x, repr (snd r) x = repr uf x } :=
   match M.get a uf.(m) with
   | Some a' =>
@@ -664,7 +664,7 @@ Next Obligation.
   destruct (find_x a')
   as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0.
   symmetry. apply repr_some. auto.
-  intros. rewrite repr_compress. 
+  intros. rewrite repr_compress.
   destruct (find_x a')
   as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto.
 Qed.
@@ -672,7 +672,7 @@ Next Obligation.
   split; auto. symmetry. apply repr_none. auto.
 Qed.
 Next Obligation.
-  apply mwf. 
+  apply mwf.
 Defined.
 
 Definition find (a: elt) : elt * t := proj1_sig (find_x a).
@@ -680,15 +680,15 @@ Definition find (a: elt) : elt * t := proj1_sig (find_x a).
 Lemma find_repr:
   forall a, fst (find a) = repr uf a.
 Proof.
-  unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. 
+  unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto.
 Qed.
 
 Lemma find_unchanged:
   forall a x, repr (snd (find a)) x = repr uf x.
 Proof.
-  unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. 
+  unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto.
 Qed.
- 
+
 Lemma sameclass_find_1:
   forall a x y, sameclass (snd (find a)) x y <-> sameclass uf x y.
 Proof.