Updated PR by removing whitespaces. Bug 17450.

1 files changed, 35 insertions, 35 deletions

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 62a0c585..a52e47bb 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -72,7 +72,7 @@ Definition wt_instr (i: instruction) : bool :=
       match is_move_operation op args with
       | Some arg =>
           subtype (mreg_type arg) (mreg_type res)
-      | None => 
+      | None =>
           let (targs, tres) := type_of_operation op in
           subtype tres (mreg_type res)
       end
@@ -105,7 +105,7 @@ Lemma wt_setreg:
   Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).
 Proof.
   intros; red; intros.
-  unfold Locmap.set. 
+  unfold Locmap.set.
   destruct (Loc.eq (R r) l).
   subst l; auto.
   destruct (Loc.diff_dec (R r) l). auto. red. auto.
@@ -116,10 +116,10 @@ Lemma wt_setstack:
   wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).
 Proof.
   intros; red; intros.
-  unfold Locmap.set. 
+  unfold Locmap.set.
   destruct (Loc.eq (S sl ofs ty) l).
-  subst l. simpl. 
-  generalize (Val.load_result_type (chunk_of_type ty) v). 
+  subst l. simpl.
+  generalize (Val.load_result_type (chunk_of_type ty) v).
   replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
   destruct ty; reflexivity.
   destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto.
@@ -164,7 +164,7 @@ Lemma wt_setlist:
 Proof.
   induction vl; destruct rl; simpl; intros; try contradiction.
   auto.
-  destruct H. apply IHvl; auto. apply wt_setreg; auto. 
+  destruct H. apply IHvl; auto. apply wt_setreg; auto.
 Qed.
 
 Lemma wt_setres:
@@ -177,7 +177,7 @@ Proof.
   induction res; simpl; intros.
 - apply wt_setreg; auto. eapply Val.has_subtype; eauto.
 - auto.
-- InvBooleans. eapply IHres2; eauto. destruct v; exact I. 
+- InvBooleans. eapply IHres2; eauto. destruct v; exact I.
   eapply IHres1; eauto. destruct v; exact I.
 Qed.
 
@@ -189,7 +189,7 @@ Lemma wt_find_label:
 Proof.
   unfold wt_function; intros until c. generalize (fn_code f). induction c0; simpl; intros.
   discriminate.
-  InvBooleans. destruct (is_label lbl a). 
+  InvBooleans. destruct (is_label lbl a).
   congruence.
   auto.
 Qed.
@@ -250,15 +250,15 @@ Hypothesis wt_prog:
 Lemma wt_find_function:
   forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f.
 Proof.
-  intros. 
+  intros.
   assert (X: exists i, In (i, Gfun f) prog.(prog_defs)).
   {
     destruct ros as [r | s]; simpl in H.
-    eapply Genv.find_funct_inversion; eauto. 
+    eapply Genv.find_funct_inversion; eauto.
     destruct (Genv.find_symbol ge s) as [b|]; try discriminate.
     eapply Genv.find_funct_ptr_inversion; eauto.
   }
-  destruct X as [i IN]. eapply wt_prog; eauto. 
+  destruct X as [i IN]. eapply wt_prog; eauto.
 Qed.
 
 Theorem step_type_preservation:
@@ -266,38 +266,38 @@ Theorem step_type_preservation:
 Proof.
   induction 1; intros WTS; inv WTS.
 - (* getstack *)
-  simpl in *; InvBooleans. 
+  simpl in *; InvBooleans.
   econstructor; eauto.
-  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS. 
+  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS.
   apply wt_undef_regs; auto.
 - (* setstack *)
-  simpl in *; InvBooleans. 
+  simpl in *; InvBooleans.
   econstructor; eauto.
   apply wt_setstack. apply wt_undef_regs; auto.
 - (* op *)
   simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE.
   + (* move *)
-    InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst. 
+    InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst.
     simpl in H. inv H.
-    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS. 
+    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS.
     apply wt_undef_regs; auto.
-  + (* other ops *) 
+  + (* other ops *)
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
     econstructor; eauto.
-    apply wt_setreg; auto. eapply Val.has_subtype; eauto. 
-    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. 
-    red; intros; subst op. simpl in ISMOVE. 
-    destruct args; try discriminate. destruct args; discriminate. 
+    apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
+    red; intros; subst op. simpl in ISMOVE.
+    destruct args; try discriminate. destruct args; discriminate.
     apply wt_undef_regs; auto.
 - (* load *)
-  simpl in *; InvBooleans. 
+  simpl in *; InvBooleans.
   econstructor; eauto.
-  apply wt_setreg. eapply Val.has_subtype; eauto. 
+  apply wt_setreg. eapply Val.has_subtype; eauto.
   destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
   apply wt_undef_regs; auto.
 - (* store *)
-  simpl in *; InvBooleans. 
-  econstructor. eauto. eauto. eauto. 
+  simpl in *; InvBooleans.
+  econstructor. eauto. eauto. eauto.
   apply wt_undef_regs; auto.
 - (* call *)
   simpl in *; InvBooleans.
@@ -305,35 +305,35 @@ Proof.
   eapply wt_find_function; eauto.
 - (* tailcall *)
   simpl in *; InvBooleans.
-  econstructor; eauto. 
+  econstructor; eauto.
   eapply wt_find_function; eauto.
-  apply wt_return_regs; auto. apply wt_parent_locset; auto. 
+  apply wt_return_regs; auto. apply wt_parent_locset; auto.
 - (* builtin *)
   simpl in *; InvBooleans.
   econstructor; eauto.
-  eapply wt_setres; eauto. eapply external_call_well_typed; eauto. 
+  eapply wt_setres; eauto. eapply external_call_well_typed; eauto.
   apply wt_undef_regs; auto.
 - (* label *)
   simpl in *. econstructor; eauto.
 - (* goto *)
-  simpl in *. econstructor; eauto. eapply wt_find_label; eauto. 
+  simpl in *. econstructor; eauto. eapply wt_find_label; eauto.
 - (* cond branch, taken *)
   simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
   apply wt_undef_regs; auto.
 - (* cond branch, not taken *)
-  simpl in *. econstructor. auto. auto. auto. 
+  simpl in *. econstructor. auto. auto. auto.
   apply wt_undef_regs; auto.
 - (* jumptable *)
   simpl in *. econstructor. auto. auto. eapply wt_find_label; eauto.
   apply wt_undef_regs; auto.
 - (* return *)
-  simpl in *. InvBooleans. 
+  simpl in *. InvBooleans.
   econstructor; eauto.
   apply wt_return_regs; auto. apply wt_parent_locset; auto.
 - (* internal function *)
   simpl in WTFD.
   econstructor. eauto. eauto. eauto.
-  apply wt_undef_regs. apply wt_call_regs. auto. 
+  apply wt_undef_regs. apply wt_call_regs. auto.
 - (* external function *)
   econstructor. auto. apply wt_setlist; auto.
   eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
@@ -344,7 +344,7 @@ Qed.
 Theorem wt_initial_state:
   forall S, initial_state prog S -> wt_state S.
 Proof.
-  induction 1. econstructor. constructor. 
+  induction 1. econstructor. constructor.
   unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
   intros [id IN]. eapply wt_prog; eauto.
   apply wt_init.
@@ -383,7 +383,7 @@ Lemma wt_state_builtin:
   wt_state (State s f sp (Lbuiltin ef args res :: c) rs m) ->
   forallb (loc_valid f) (params_of_builtin_args args) = true.
 Proof.
-  intros. inv H. simpl in WTC; InvBooleans. auto. 
+  intros. inv H. simpl in WTC; InvBooleans. auto.
 Qed.
 
 Lemma wt_callstate_wt_regs:
@@ -391,5 +391,5 @@ Lemma wt_callstate_wt_regs:
   wt_state (Callstate s f rs m) ->
   forall r, Val.has_type (rs (R r)) (mreg_type r).
 Proof.
-  intros. inv H. apply WTRS. 
+  intros. inv H. apply WTRS.
 Qed.