Updated PR by removing whitespaces. Bug 17450.

1 files changed, 38 insertions, 38 deletions

diff --git a/lib/Lattice.v b/lib/Lattice.v
index 5a941a13..352b4479 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -27,7 +27,7 @@ Local Unset Case Analysis Schemes.
 (** * Signatures of semi-lattices *)
 
 (** A semi-lattice is a type [t] equipped with an equivalence relation [eq],
-  a boolean equivalence test [beq], a partial order [ge], a smallest element 
+  a boolean equivalence test [beq], a partial order [ge], a smallest element
   [bot], and an upper bound operation [lub].
   Note that we do not demand that [lub] computes the least upper bound. *)
 
@@ -86,9 +86,9 @@ Lemma gsspec:
   forall p v x q,
   L.eq (get q (set p v x)) (if peq q p then v else get q x).
 Proof.
-  intros. unfold set, get. 
+  intros. unfold set, get.
   destruct (L.beq v L.bot) eqn:EBOT.
-  rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). 
+  rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p).
   apply L.eq_sym. apply L.beq_correct; auto.
   apply L.eq_refl.
   rewrite PTree.gsspec. destruct (peq q p); apply L.eq_refl.
@@ -117,7 +117,7 @@ Definition beq (x y: t) : bool := PTree.beq L.beq x y.
 Lemma beq_correct: forall x y, beq x y = true -> eq x y.
 Proof.
   unfold beq; intros; red; intros. unfold get.
-  rewrite PTree.beq_correct in H. specialize (H p). 
+  rewrite PTree.beq_correct in H. specialize (H p).
   destruct (x!p); destruct (y!p); intuition.
   apply L.beq_correct; auto.
   apply L.eq_refl.
@@ -165,17 +165,17 @@ Definition opt_eq (ox oy: option L.t) : Prop :=
 
 Lemma opt_eq_refl: forall ox, opt_eq ox ox.
 Proof.
-  intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto. 
+  intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto.
 Qed.
 
 Lemma opt_eq_sym: forall ox oy, opt_eq ox oy -> opt_eq oy ox.
 Proof.
-  unfold opt_eq. destruct ox; destruct oy; auto. apply L.eq_sym. 
+  unfold opt_eq. destruct ox; destruct oy; auto. apply L.eq_sym.
 Qed.
 
 Lemma opt_eq_trans: forall ox oy oz, opt_eq ox oy -> opt_eq oy oz -> opt_eq ox oz.
 Proof.
-  unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition. 
+  unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition.
   eapply L.eq_trans; eauto.
 Qed.
 
@@ -189,8 +189,8 @@ Definition opt_beq (ox oy: option L.t) : bool :=
 Lemma opt_beq_correct:
   forall ox oy, opt_beq ox oy = true -> opt_eq ox oy.
 Proof.
-  unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence. 
-  intros. apply L.beq_correct; auto. 
+  unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence.
+  intros. apply L.beq_correct; auto.
   auto.
 Qed.
 
@@ -206,7 +206,7 @@ Proof. intros; red; intros; apply opt_eq_sym; auto. Qed.
 Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3.
 Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed.
 
-Lemma tree_eq_node: 
+Lemma tree_eq_node:
   forall l1 o1 r1 l2 o2 r2,
   tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
   tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2).
@@ -214,23 +214,23 @@ Proof.
   intros; red; intros. destruct i; simpl; auto.
 Qed.
 
-Lemma tree_eq_node': 
+Lemma tree_eq_node':
   forall l1 o1 r1 l2 o2 r2,
   tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
   tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2).
 Proof.
-  intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. 
+  intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto.
 Qed.
 
-Lemma tree_eq_node'': 
+Lemma tree_eq_node'':
   forall l1 o1 r1 l2 o2 r2,
   tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
   tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2).
 Proof.
-  intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. 
+  intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto.
 Qed.
 
-Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym 
+Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym
              tree_eq_refl tree_eq_sym
              tree_eq_node tree_eq_node' tree_eq_node'' : combine.
 
@@ -296,7 +296,7 @@ Inductive changed2 : Type :=
 
 Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 :=
     match m1, m2 with
-    | PTree.Leaf, PTree.Leaf => 
+    | PTree.Leaf, PTree.Leaf =>
         Same
     | PTree.Leaf, _ =>
         match combine_r m2 with
@@ -333,7 +333,7 @@ Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 :=
     end.
 
 Lemma xcombine_eq:
-  forall m1 m2, 
+  forall m1 m2,
   match xcombine m1 m2 with
   | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2)
   | Same1 => tree_eq m1 (PTree.combine f m1 m2)
@@ -348,7 +348,7 @@ Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r.
   destruct (combine_r (PTree.Node m2_1 o m2_2)); auto.
   generalize (combine_l_eq (PTree.Node m1_1 o m1_2)).
   destruct (combine_l (PTree.Node m1_1 o m1_2)); auto.
-  generalize (IHm1_1 m2_1) (IHm1_2 m2_2). 
+  generalize (IHm1_1 m2_1) (IHm1_2 m2_2).
   destruct (xcombine m1_1 m2_1);
   destruct (xcombine m1_2 m2_2); auto with combine;
   intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine.
@@ -390,7 +390,7 @@ Lemma gcombine_bot:
   L.eq (get p (combine f t1 t2))
        (match f t1!p t2!p with Some x => x | None => L.bot end).
 Proof.
-  intros. unfold get. generalize (gcombine f H t1 t2 p). unfold opt_eq. 
+  intros. unfold get. generalize (gcombine f H t1 t2 p). unfold opt_eq.
   destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p).
   auto. contradiction. contradiction. intros; apply L.eq_refl.
 Qed.
@@ -398,9 +398,9 @@ Qed.
 Lemma ge_lub_left:
   forall x y, ge (lub x y) x.
 Proof.
-  unfold ge, lub; intros. 
+  unfold ge, lub; intros.
   eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto.
-  unfold get. destruct x!p. destruct y!p. 
+  unfold get. destruct x!p. destruct y!p.
   apply L.ge_lub_left.
   apply L.ge_refl. apply L.eq_refl.
   apply L.ge_bot.
@@ -409,9 +409,9 @@ Qed.
 Lemma ge_lub_right:
   forall x y, ge (lub x y) y.
 Proof.
-  unfold ge, lub; intros. 
+  unfold ge, lub; intros.
   eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto.
-  unfold get. destruct y!p. destruct x!p. 
+  unfold get. destruct y!p. destruct x!p.
   apply L.ge_lub_right.
   apply L.ge_refl. apply L.eq_refl.
   apply L.ge_bot.
@@ -451,11 +451,11 @@ Lemma gsspec:
   x <> Bot -> ~L.eq v L.bot ->
   L.eq (get q (set p v x)) (if peq q p then v else get q x).
 Proof.
-  intros. unfold set. destruct x. congruence. 
-  destruct (L.beq v L.bot) eqn:EBOT. 
+  intros. unfold set. destruct x. congruence.
+  destruct (L.beq v L.bot) eqn:EBOT.
   elim H0. apply L.beq_correct; auto.
   destruct (L.beq v L.top) eqn:ETOP; simpl.
-  rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). 
+  rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p).
   apply L.eq_sym. apply L.beq_correct; auto.
   apply L.eq_refl.
   rewrite PTree.gsspec. destruct (peq q p); apply L.eq_refl.
@@ -561,7 +561,7 @@ Lemma gcombine_top:
   L.eq (get p (Top_except (LM.combine f t1 t2)))
        (match f t1!p t2!p with Some x => x | None => L.top end).
 Proof.
-  intros. simpl. generalize (LM.gcombine f H t1 t2 p). unfold LM.opt_eq. 
+  intros. simpl. generalize (LM.gcombine f H t1 t2 p). unfold LM.opt_eq.
   destruct ((LM.combine f t1 t2)!p); destruct (f t1!p t2!p).
   auto. contradiction. contradiction. intros; apply L.eq_refl.
 Qed.
@@ -574,10 +574,10 @@ Proof.
   rewrite get_bot. apply L.ge_bot.
   apply L.ge_refl. apply L.eq_refl.
   eapply L.ge_trans. apply L.ge_refl. apply gcombine_top; auto.
-  unfold get. destruct t0!p. destruct t1!p. 
+  unfold get. destruct t0!p. destruct t1!p.
   unfold opt_lub. destruct (L.beq (L.lub t2 t3) L.top) eqn:E.
-  apply L.ge_top. apply L.ge_lub_left. 
-  apply L.ge_top. 
+  apply L.ge_top. apply L.ge_lub_left.
+  apply L.ge_top.
   apply L.ge_top.
 Qed.
 
@@ -589,10 +589,10 @@ Proof.
   apply L.ge_refl. apply L.eq_refl.
   rewrite get_bot. apply L.ge_bot.
   eapply L.ge_trans. apply L.ge_refl. apply gcombine_top; auto.
-  unfold get. destruct t0!p; destruct t1!p. 
+  unfold get. destruct t0!p; destruct t1!p.
   unfold opt_lub. destruct (L.beq (L.lub t2 t3) L.top) eqn:E.
-  apply L.ge_top. apply L.ge_lub_right. 
-  apply L.ge_top. 
+  apply L.ge_top. apply L.ge_lub_right.
+  apply L.ge_top.
   apply L.ge_top.
   apply L.ge_top.
 Qed.
@@ -618,7 +618,7 @@ Module LFSet (S: FSetInterface.WS) <: SEMILATTICE.
   Definition ge (x y: t) := S.Subset y x.
   Lemma ge_refl: forall x y, eq x y -> ge x y.
   Proof.
-    unfold eq, ge, S.Equal, S.Subset; intros. firstorder. 
+    unfold eq, ge, S.Equal, S.Subset; intros. firstorder.
   Qed.
   Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
   Proof.
@@ -635,12 +635,12 @@ Module LFSet (S: FSetInterface.WS) <: SEMILATTICE.
 
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
-    unfold lub, ge, S.Subset; intros. apply S.union_2; auto. 
+    unfold lub, ge, S.Subset; intros. apply S.union_2; auto.
   Qed.
 
   Lemma ge_lub_right: forall x y, ge (lub x y) y.
   Proof.
-    unfold lub, ge, S.Subset; intros. apply S.union_3; auto. 
+    unfold lub, ge, S.Subset; intros. apply S.union_3; auto.
   Qed.
 
 End LFSet.
@@ -650,7 +650,7 @@ End LFSet.
 (** Given a type with decidable equality [X], the following functor
   returns a semi-lattice structure over [X.t] complemented with
   a top and a bottom element.  The ordering is the flat ordering
-  [Bot < Inj x < Top]. *) 
+  [Bot < Inj x < Top]. *)
 
 Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.
 
@@ -735,7 +735,7 @@ Proof.
 Qed.
 
 End LFlat.
-  
+
 (** * Boolean semi-lattice *)
 
 (** This semi-lattice has only two elements, [bot] and [top], trivially