1 files changed, 17 insertions, 17 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index beb29965..2a63b1d5 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -161,7 +161,7 @@ Proof.
   intros until valu. unfold max_over_list.
   assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z).
   induction l; simpl; intros.
-  omega. apply Zge_trans with (Zmax z (valu a)). 
+  omega. apply Zge_trans with (Zmax z (valu a)).
   auto. apply Zle_ge. apply Zmax1. auto.
 Qed.
 
@@ -193,7 +193,7 @@ Program Definition function_bounds :=
     _ _.
 Next Obligation.
   apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
-  apply Zge_le. apply max_over_slots_of_funct_pos.  
+  apply Zge_le. apply max_over_slots_of_funct_pos.
 Qed.
 Next Obligation.
   apply Zle_ge. apply Zmax2.
@@ -211,10 +211,10 @@ Proof.
             z <= f /\ (In x c -> valu x <= f)).
     induction c; simpl; intros.
     split. omega. tauto.
-    elim (IHc (Zmax z (valu a))); intros. 
-    split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto. 
-    intro H1; elim H1; intro. 
-    subst a. apply Zle_trans with (Zmax z (valu x)). 
+    elim (IHc (Zmax z (valu a))); intros.
+    split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto.
+    intro H1; elim H1; intro.
+    subst a. apply Zle_trans with (Zmax z (valu x)).
     apply Zmax2. auto. auto.
   intro. elim (H l 0); intros. auto.
 Qed.
@@ -231,7 +231,7 @@ Lemma max_over_regs_of_funct_bound:
   In i f.(fn_code) -> In r (regs_of_instr i) ->
   valu r <= max_over_regs_of_funct valu.
 Proof.
-  intros. unfold max_over_regs_of_funct. 
+  intros. unfold max_over_regs_of_funct.
   apply Zle_trans with (max_over_regs_of_instr valu i).
   unfold max_over_regs_of_instr. apply max_over_list_bound. auto.
   apply max_over_instrs_bound. auto.
@@ -242,7 +242,7 @@ Lemma max_over_slots_of_funct_bound:
   In i f.(fn_code) -> In s (slots_of_instr i) ->
   valu s <= max_over_slots_of_funct valu.
 Proof.
-  intros. unfold max_over_slots_of_funct. 
+  intros. unfold max_over_slots_of_funct.
   apply Zle_trans with (max_over_slots_of_instr valu i).
   unfold max_over_slots_of_instr. apply max_over_list_bound. auto.
   apply max_over_instrs_bound. auto.
@@ -255,7 +255,7 @@ Lemma int_callee_save_bound:
 Proof.
   intros. apply Zlt_le_trans with (int_callee_save r).
   unfold int_callee_save. omega.
-  unfold function_bounds, bound_int_callee_save. 
+  unfold function_bounds, bound_int_callee_save.
   eapply max_over_regs_of_funct_bound; eauto.
 Qed.
 
@@ -266,7 +266,7 @@ Lemma float_callee_save_bound:
 Proof.
   intros. apply Zlt_le_trans with (float_callee_save r).
   unfold float_callee_save. omega.
-  unfold function_bounds, bound_float_callee_save. 
+  unfold function_bounds, bound_float_callee_save.
   eapply max_over_regs_of_funct_bound; eauto.
 Qed.
 
@@ -315,11 +315,11 @@ Proof.
 Qed.
 
 Lemma slot_is_within_bounds:
-  forall i, In i f.(fn_code) -> 
+  forall i, In i f.(fn_code) ->
   forall sl ty ofs, In (sl, ofs, ty) (slots_of_instr i) ->
   slot_within_bounds function_bounds sl ofs ty.
 Proof.
-  intros. unfold slot_within_bounds. 
+  intros. unfold slot_within_bounds.
   destruct sl.
   eapply local_slot_bound; eauto.
   auto.
@@ -329,12 +329,12 @@ Qed.
 Lemma slots_of_locs_charact:
   forall sl ofs ty l, In (sl, ofs, ty) (slots_of_locs l) <-> In (S sl ofs ty) l.
 Proof.
-  induction l; simpl; intros. 
+  induction l; simpl; intros.
   tauto.
   destruct a; simpl; intuition congruence.
 Qed.
 
-(** It follows that every instruction in the function is within bounds, 
+(** It follows that every instruction in the function is within bounds,
     in the sense of the [instr_within_bounds] predicate. *)
 
 Lemma instr_is_within_bounds:
@@ -342,16 +342,16 @@ Lemma instr_is_within_bounds:
   In i f.(fn_code) ->
   instr_within_bounds function_bounds i.
 Proof.
-  intros; 
+  intros;
   destruct i;
-  generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); 
+  generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H);
   simpl; intros; auto.
 (* call *)
   eapply size_arguments_bound; eauto.
 (* builtin *)
   split; intros.
   apply H1. apply in_or_app; auto.
-  apply H0. rewrite slots_of_locs_charact; auto. 
+  apply H0. rewrite slots_of_locs_charact; auto.
 Qed.
 
 Lemma function_is_within_bounds: