Updated PR by removing whitespaces. Bug 17450.

1 files changed, 37 insertions, 37 deletions

diff --git a/common/AST.v b/common/AST.v
index c62b0091..16673c47 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -121,7 +121,7 @@ Definition proj_sig_res (s: signature) : typ :=
 Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
 Proof.
   generalize opt_typ_eq, list_typ_eq; intros; decide equality.
-  generalize bool_dec; intros. decide equality. 
+  generalize bool_dec; intros. decide equality.
 Defined.
 Global Opaque signature_eq.
 
@@ -255,14 +255,14 @@ Lemma transform_program_function:
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf.
 Proof.
   simpl. unfold transform_program. intros.
-  exploit list_in_map_inv; eauto. 
-  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. 
+  exploit list_in_map_inv; eauto.
+  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ.
   exists f; auto.
 Qed.
 
 End TRANSF_PROGRAM.
 
-(** General iterator over program that applies a given code transfomration 
+(** General iterator over program that applies a given code transfomration
     function to all function descriptions with their identifers and leaves
     teh other parts of the program unchanged. *)
 
@@ -289,18 +289,18 @@ Lemma tranforma_program_function_ident:
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf.
 Proof.
   simpl. unfold transform_program_ident. intros.
-  exploit list_in_map_inv; eauto. 
-  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. 
+  exploit list_in_map_inv; eauto.
+  intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ.
   exists f; auto.
 Qed.
 
 End TRANSF_PROGRAM_IDENT.
 
-(** The following is a more general presentation of [transform_program] where 
+(** The following is a more general presentation of [transform_program] where
   global variable information can be transformed, in addition to function
   definitions.  Moreover, the transformation functions can fail and
   return an error message. Also the transformation functions are defined
-  for the case the identifier of the function is passed as additional 
+  for the case the identifier of the function is passed as additional
   argument *)
 
 Local Open Scope error_monad_scope.
@@ -338,7 +338,7 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl
       end
   end.
 
-Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := 
+Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
   match l with
   | nil => OK nil
   | (id, Gfun f) :: l' =>
@@ -369,12 +369,12 @@ Lemma transform_partial_program2_function:
   In (i, Gfun tf) tp.(prog_defs) ->
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf.
 Proof.
-  intros. monadInv H. simpl in H0. 
+  intros. monadInv H. simpl in H0.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
   destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H. exists f; auto. 
+  simpl in H0; destruct H0. inv H. exists f; auto.
   exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
   destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H.
@@ -387,12 +387,12 @@ Lemma transform_partial_ident_program2_function:
   In (i, Gfun tf) tp.(prog_defs) ->
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf.
 Proof.
-  intros. monadInv H. simpl in H0. 
+  intros. monadInv H. simpl in H0.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
   destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ.
-  simpl in H0; destruct H0. inv H. exists f; auto. 
+  simpl in H0; destruct H0. inv H. exists f; auto.
   exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto.
   destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ.
   simpl in H0; destruct H0. inv H.
@@ -407,7 +407,7 @@ Lemma transform_partial_program2_variable:
      In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
   /\ transf_var v = OK tv.(gvar_info).
 Proof.
-  intros. monadInv H. simpl in H0. 
+  intros. monadInv H. simpl in H0.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
@@ -429,7 +429,7 @@ Lemma transform_partial_ident_program2_variable:
      In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs)
   /\ transf_var_ident i v = OK tv.(gvar_info).
 Proof.
-  intros. monadInv H. simpl in H0. 
+  intros. monadInv H. simpl in H0.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   inv EQ. contradiction.
   destruct a as [id [f|v]].
@@ -451,11 +451,11 @@ Lemma transform_partial_program2_succeeds:
   | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv
   end.
 Proof.
-  intros. monadInv H. 
+  intros. monadInv H.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   contradiction.
   destruct a as [id1 g1]. destruct g1.
-  destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. 
+  destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ.
   destruct H0. inv H. econstructor; eauto. eapply IHl; eauto.
   destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ.
   destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto.
@@ -470,11 +470,11 @@ Lemma transform_partial_ident_program2_succeeds:
   | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv
   end.
 Proof.
-  intros. monadInv H. 
+  intros. monadInv H.
   revert x EQ H0. induction (prog_defs p); simpl; intros.
   contradiction.
   destruct a as [id1 g1]. destruct g1.
-  destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ. 
+  destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ.
   destruct H0. inv H. econstructor; eauto. eapply IHl; eauto.
   destruct (transf_globvar_ident id1 v) eqn:TV; try discriminate. monadInv EQ.
   destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto.
@@ -621,7 +621,7 @@ Lemma transform_partial_program_function:
   In (i, Gfun tf) tp.(prog_defs) ->
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf.
 Proof.
-  apply transform_partial_program2_function. 
+  apply transform_partial_program2_function.
 Qed.
 
 Lemma transform_partial_ident_program_function:
@@ -630,7 +630,7 @@ Lemma transform_partial_ident_program_function:
   In (i, Gfun tf) tp.(prog_defs) ->
   exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf.
 Proof.
-  apply transform_partial_ident_program2_function. 
+  apply transform_partial_ident_program2_function.
 Qed.
 
 Lemma transform_partial_program_succeeds:
@@ -639,8 +639,8 @@ Lemma transform_partial_program_succeeds:
   In (i, Gfun fd) p.(prog_defs) ->
   exists tfd, transf_partial fd = OK tfd.
 Proof.
-  unfold transform_partial_program; intros. 
-  exploit transform_partial_program2_succeeds; eauto. 
+  unfold transform_partial_program; intros.
+  exploit transform_partial_program2_succeeds; eauto.
 Qed.
 
 Lemma transform_partial_ident_program_succeeds:
@@ -649,8 +649,8 @@ Lemma transform_partial_ident_program_succeeds:
   In (i, Gfun fd) p.(prog_defs) ->
   exists tfd, transf_partial_ident i fd = OK tfd.
 Proof.
-  unfold transform_partial_ident_program; intros. 
-  exploit transform_partial_ident_program2_succeeds; eauto. 
+  unfold transform_partial_ident_program; intros.
+  exploit transform_partial_ident_program2_succeeds; eauto.
 Qed.
 
 End TRANSF_PARTIAL_PROGRAM.
@@ -663,7 +663,7 @@ Proof.
   unfold transform_partial_program, transform_partial_program2, transform_program; intros.
   replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs))
      with (OK (map (transform_program_globdef transf) p.(prog_defs))).
-  auto. 
+  auto.
   induction (prog_defs p); simpl.
   auto.
   destruct a as [id [f|v]]; rewrite <- IHl.
@@ -679,7 +679,7 @@ Proof.
   unfold transform_partial_ident_program, transform_partial_ident_program2, transform_program; intros.
   replace (transf_globdefs_ident (fun id f => OK (transf id f)) (fun _  v => OK v) p.(prog_defs))
      with (OK (map (transform_program_globdef_ident transf) p.(prog_defs))).
-  auto. 
+  auto.
   induction (prog_defs p); simpl.
   auto.
   destruct a as [id [f|v]]; rewrite <- IHl.
@@ -687,11 +687,11 @@ Proof.
     destruct v; auto.
 Qed.
 
-(** The following is a relational presentation of 
+(** The following is a relational presentation of
   [transform_partial_augment_preogram].  Given relations between function
   definitions and between variable information, it defines a relation
   between programs stating that the two programs have appropriately related
-  shapes (global names are preserved and possibly augmented, etc) 
+  shapes (global names are preserved and possibly augmented, etc)
   and that identically-named function definitions
   and variable information are related. *)
 
@@ -723,24 +723,24 @@ Lemma transform_partial_augment_program_match:
   forall (A B V W: Type)
          (transf_fun: A -> res B)
          (transf_var: V -> res W)
-         (p: program A V) 
+         (p: program A V)
          (new_globs : list (ident * globdef B W))
          (new_main : ident)
          (tp: program B W),
   transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp ->
-  match_program 
+  match_program
     (fun fd tfd => transf_fun fd = OK tfd)
     (fun info tinfo => transf_var info = OK tinfo)
     new_globs new_main
     p tp.
 Proof.
-  unfold transform_partial_augment_program; intros. monadInv H. 
+  unfold transform_partial_augment_program; intros. monadInv H.
   red; simpl. split; auto. exists x; split; auto.
   revert x EQ. generalize (prog_defs p). induction l; simpl; intros.
   monadInv EQ. constructor.
-  destruct a as [id [f|v]]. 
+  destruct a as [id [f|v]].
   (* function *)
-  destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. 
+  destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ.
   constructor; auto. constructor; auto.
   (* variable *)
   unfold transf_globvar in EQ.
@@ -890,7 +890,7 @@ End TRANSF_PARTIAL_FUNDEF.
 
 (** * Arguments and results to builtin functions *)
 
-Set Contextual Implicit. 
+Set Contextual Implicit.
 
 Inductive builtin_arg (A: Type) : Type :=
   | BA (x: A)
@@ -948,7 +948,7 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar
   | BA_addrstack ofs => BA_addrstack ofs
   | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
   | BA_addrglobal id ofs => BA_addrglobal id ofs
-  | BA_splitlong hi lo => 
+  | BA_splitlong hi lo =>
       BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
   end.
 
@@ -956,7 +956,7 @@ Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_re
   match a with
   | BR x => BR (f x)
   | BR_none => BR_none
-  | BR_splitlong hi lo => 
+  | BR_splitlong hi lo =>
       BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
   end.