Remove usage of do.

Apparently coq compiled with camlp4 has a problem with the user
defined do <- ... ; ... and do.
Bug 20050

3 files changed, 121 insertions, 122 deletions

diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 3a35b87e..4f8632f2 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -37,7 +37,7 @@ Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.
   unfold transl_program; intros.
-  eapply match_transform_partial_program2. 
+  eapply match_transform_partial_program2.
   eexact H.
 - intros. destruct f; simpl in H0.
 + monadInv H0. constructor; auto.
@@ -109,7 +109,7 @@ Lemma transl_alignof_blockcopy:
 Proof.
   intros. destruct H.
   unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
-  split. 
+  split.
 - symmetry. apply Ctypes.sizeof_stable; auto.
 - revert C. induction t; simpl; auto;
   destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
@@ -119,10 +119,10 @@ Lemma field_offset_stable:
   forall (cunit prog: Clight.program) id co f,
   linkorder cunit prog ->
   cunit.(prog_comp_env)!id = Some co ->
-  prog.(prog_comp_env)!id = Some co /\ 
+  prog.(prog_comp_env)!id = Some co /\
   field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co).
 Proof.
-  intros. 
+  intros.
   assert (C: composite_consistent cunit.(prog_comp_env) co).
   { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
     apply prog_comp_env_eq. }
@@ -134,7 +134,7 @@ Proof.
   rewrite ! (alignof_stable _ _ A) by auto.
   rewrite ! (sizeof_stable _ _ A) by auto.
   destruct (ident_eq f f1); eauto.
-Qed. 
+Qed.
 
 (** * Properties of the translation functions *)
 
@@ -329,7 +329,7 @@ Lemma make_cmpu_ne_zero_correct_ptr:
   Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true ->
   eval_expr ge e le m (make_cmpu_ne_zero a) Vone.
 Proof.
-  intros. 
+  intros.
   assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone).
   { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
     unfold Mem.weak_valid_pointer in H1. rewrite H0, H1.
@@ -343,8 +343,8 @@ Proof.
 - inv H; eelim OF_OPTBOOL; eauto.
 - inv H; eelim OF_OPTBOOL; eauto.
 - inv H; eelim OF_OPTBOOL; eauto.
-- inv H; eelim OF_BOOL; eauto. 
-- inv H; eelim OF_BOOL; eauto. 
+- inv H; eelim OF_BOOL; eauto.
+- inv H; eelim OF_BOOL; eauto.
 Qed.
 
 Lemma make_cast_int_correct:
@@ -365,7 +365,7 @@ Lemma make_longofint_correct:
   eval_expr ge e le m a (Vint n) ->
   eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)).
 Proof.
-  intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. 
+  intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm.
 Qed.
 
 Hint Resolve make_cast_int_correct make_longofint_correct: cshm.
@@ -448,13 +448,13 @@ Proof.
   econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto.
   destruct (Int.eq i Int.zero); simpl; constructor.
 - (* ptr 32 bits *)
-  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. 
+  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor.
 - (* long *)
   econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto.
   destruct (Int64.eq i Int64.zero); simpl; constructor.
 - (* ptr 64 bits *)
-  exists Vone; split. 
-  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. 
+  exists Vone; split.
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
   unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity.
   constructor.
 - (* float *)
@@ -501,21 +501,21 @@ Lemma make_notbool_correct:
 Proof.
   unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1.
   destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval.
-- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. 
+- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
   destruct (Int.eq i Int.zero); auto.
 - destruct Archi.ptr64 eqn:SF; inv SEM.
   destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
-  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. 
+  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
   unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto.
-- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. 
+- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
   destruct (Int64.eq i Int64.zero); auto.
 - destruct Archi.ptr64 eqn:SF; inv SEM.
   destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
-  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. 
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
   unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto.
-- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. 
+- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool.
   destruct (Float.cmp Ceq f Float.zero); auto.
-- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. 
+- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool.
   destruct (Float32.cmp Ceq f Float32.zero); auto.
 Qed.
 
@@ -633,7 +633,7 @@ Lemma ptrofs_mul_32:
   Archi.ptr64 = false ->
   Ptrofs.of_int (Int.mul (Int.repr n) i) = Ptrofs.mul (Ptrofs.repr n) (ptrofs_of_int si i).
 Proof.
-  intros. apply Ptrofs.eqm_samerepr. 
+  intros. apply Ptrofs.eqm_samerepr.
   eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ].
   apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
   apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
@@ -646,11 +646,11 @@ Lemma ptrofs_mul_32_64:
   Archi.ptr64 = false ->
   Ptrofs.of_int (Int.mul (Int.repr n) (Int64.loword i)) = Ptrofs.mul (Ptrofs.repr n) (Ptrofs.of_int64 i).
 Proof.
-  intros. apply Ptrofs.eqm_samerepr. 
+  intros. apply Ptrofs.eqm_samerepr.
   eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ].
   apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
   apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-  unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. 
+  unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r.
   unfold Int64.loword. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
 Qed.
 *)
@@ -663,20 +663,20 @@ Proof.
 - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
   econstructor; eauto with cshm.
-  simpl. rewrite SF. do 3 f_equal. 
+  simpl. rewrite SF. apply f_equal.  apply f_equal.  apply f_equal.
   assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
   { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
   auto with ptrofs.
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
-  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
   auto with ptrofs.
 - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
   econstructor; eauto with cshm.
-  simpl. rewrite SF. do 3 f_equal. auto with ptrofs.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
-  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
   auto with ptrofs.
 - eapply make_binarith_correct; eauto; intros; auto.
@@ -690,17 +690,17 @@ Proof.
 - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
   econstructor; eauto with cshm.
-  simpl. rewrite SF. do 3 f_equal. 
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
   { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
   auto with ptrofs.
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
-  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
   auto with ptrofs.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. 
+- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ.
   set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
-  destruct va; InvEval; destruct vb; InvEval. 
+  destruct va; InvEval; destruct vb; InvEval.
   destruct (eq_block b0 b1); try discriminate.
   destruct (zlt 0 sz); try discriminate.
   destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
@@ -709,37 +709,37 @@ Proof.
   destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
 + assert (E: Int64.signed (Int64.repr sz) = sz).
   { apply Int64.signed_repr.
-    replace Int64.max_signed with Ptrofs.max_signed. 
+    replace Int64.max_signed with Ptrofs.max_signed.
     generalize Int64.min_signed_neg; omega.
     unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
   econstructor; eauto with cshm.
-  rewrite SF, dec_eq_true. simpl. 
+  rewrite SF, dec_eq_true. simpl.
   predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
   rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction.
   predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
   rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction.
-  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal.
-  symmetry. auto with ptrofs.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal.
+  apply f_equal. symmetry. auto with ptrofs.
 + assert (E: Int.signed (Int.repr sz) = sz).
   { apply Int.signed_repr.
-    replace Int.max_signed with Ptrofs.max_signed. 
+    replace Int.max_signed with Ptrofs.max_signed.
     generalize Int.min_signed_neg; omega.
-    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. 
+    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity.
   }
-  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. 
+  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
   rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
   rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
-  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal.
   symmetry. auto with ptrofs.
 - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
   econstructor; eauto with cshm.
-  simpl. rewrite SF. do 3 f_equal. 
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   auto with ptrofs.
 + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
-  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
   assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
   auto with ptrofs.
 - eapply make_binarith_correct; eauto; intros; auto.
@@ -867,7 +867,7 @@ Proof.
   unfold cmp_ptr, make_cmp_ptr; intros.
   destruct Archi.ptr64.
 - econstructor; eauto.
-- econstructor; eauto. simpl. unfold Val.cmpu. 
+- econstructor; eauto. simpl. unfold Val.cmpu.
   destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto.
 Qed.
 
@@ -880,15 +880,15 @@ Proof.
 - unfold make_longofint. destruct si.
 + replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)).
   eauto with cshm.
-  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. 
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
 + replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)).
   eauto with cshm.
-  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. 
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
 - destruct si.
 + replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto.
-  symmetry. auto with ptrofs. 
+  symmetry. auto with ptrofs.
 + replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto.
-  symmetry. auto with ptrofs. 
+  symmetry. auto with ptrofs.
 Qed.
 
 Remark make_ptrofs_of_int64_correct:
@@ -899,7 +899,7 @@ Proof.
   intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF.
 - replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto.
   symmetry. auto with ptrofs.
-- econstructor; eauto. simpl. do 2 f_equal.
+- econstructor; eauto. simpl. apply f_equal. apply f_equal.
   apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr.
 Qed.
 
@@ -983,7 +983,7 @@ Lemma make_memcpy_correct:
   step ge (State f s k e le m) E0 (State f Sskip k e le m').
 Proof.
   intros. inv H1; try congruence.
-  monadInv H3. 
+  monadInv H3.
   exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
   change le with (set_optvar None Vundef le) at 2.
   econstructor.
@@ -1131,8 +1131,8 @@ Lemma match_env_alloc_variables:
 Proof.
   induction 2; simpl; intros.
 - inv H0. exists te1; split. constructor. auto.
-- monadInv H2. monadInv EQ. simpl in *. 
-  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. 
+- monadInv H2. monadInv EQ. simpl in *.
+  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ.
   exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)).
   auto.
   constructor.
@@ -1254,7 +1254,7 @@ Proof.
 - (* deref *)
   simpl in TR. eauto.
 - (* field struct *)
-  unfold make_field_access in EQ0. rewrite H1 in EQ0. 
+  unfold make_field_access in EQ0. rewrite H1 in EQ0.
   destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
   exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
   rewrite <- B in EQ1.
@@ -1262,9 +1262,9 @@ Proof.
   subst x0.
   destruct Archi.ptr64 eqn:SF.
 + eapply eval_Ebinop; eauto using make_longconst_correct.
-  simpl. rewrite SF. do 3 f_equal. auto with ptrofs. 
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
 + eapply eval_Ebinop; eauto using make_intconst_correct.
-  simpl. rewrite SF. do 3 f_equal. auto with ptrofs.
+  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
 - (* field union *)
   unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
   auto.
@@ -1570,7 +1570,7 @@ Proof.
   rewrite H in CF. simpl in CF. inv CF.
   econstructor; split.
   apply plus_one. econstructor; eauto.
-  eapply transl_expr_correct with (cunit := cu); eauto. 
+  eapply transl_expr_correct with (cunit := cu); eauto.
   eapply transl_arglist_correct with (cunit := cu); eauto.
   erewrite typlist_of_arglist_eq by eauto.
   eapply transl_fundef_sig1; eauto.
@@ -1739,7 +1739,7 @@ Proof.
   econstructor; eauto. constructor.
 
 - (* internal function *)
-  inv H. inv TR. monadInv H5. 
+  inv H. inv TR. monadInv H5.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   exploit match_env_alloc_variables; eauto.
   apply match_env_empty.
@@ -1749,7 +1749,7 @@ Proof.
   simpl. erewrite transl_vars_names by eauto. assumption.
   simpl. assumption.
   simpl. assumption.
-  simpl; eauto. 
+  simpl; eauto.
   simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
   simpl. econstructor; eauto.
   unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
@@ -1809,7 +1809,7 @@ End CORRECTNESS.
 Instance TransfCshmgenLink : TransfLink match_prog.
 Proof.
   red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
-  generalize H. 
+  generalize H.
 Local Transparent Ctypes.Linker_program.
   simpl; unfold link_program.
   destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
@@ -1819,15 +1819,15 @@ Local Transparent Ctypes.Linker_program.
            (prog_comp_env_eq p2) EQ) as (env & P & Q).
   intros E.
   eapply Linking.link_match_program; eauto.
-- intros. 
+- intros.
 Local Transparent Linker_fundef Linking.Linker_fundef.
-  inv H3; inv H4; simpl in H2. 
+  inv H3; inv H4; simpl in H2.
 + discriminate.
 + destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto.
 + destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto.
 + destruct (external_function_eq ef ef0 && typelist_eq args args0 &&
          type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2.
-  InvBooleans. subst ef0. econstructor; split. 
+  InvBooleans. subst ef0. econstructor; split.
   simpl; rewrite dec_eq_true; eauto.
   left; constructor. congruence.
 - intros. exists tt. auto.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 99d0680d..4effe7c9 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -142,7 +142,7 @@ Proof.
             || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK;
   try (intuition discriminate).
   intros _.
-  InvBooleans. 
+  InvBooleans.
   exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto.
   rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods.
   red; intros; subst i0; rewrite Int.eq_true in H; discriminate.
@@ -182,7 +182,7 @@ Proof.
             || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone) eqn:OK;
   try (intuition discriminate).
   intros _.
-  InvBooleans. 
+  InvBooleans.
   exists (Int64.shr i (Int64.repr 63)), i, i0, (Int64.divs i i0), (Int64.mods i i0); intuition auto.
   rewrite Int64.shr_lt_zero. apply Int64.divmods2_divs_mods.
   red; intros; subst i0; rewrite Int64.eq_true in H; discriminate.
@@ -314,7 +314,7 @@ Proof.
   unfold mk_storebyte; intros.
   destruct (Archi.ptr64 || low_ireg r) eqn:E.
 (* low reg *)
-  monadInv H. econstructor; split. apply exec_straight_one. 
+  monadInv H. econstructor; split. apply exec_straight_one.
   simpl. unfold exec_store. rewrite H0. eauto. auto.
   intros; Simplifs.
 (* high reg *)
@@ -333,7 +333,7 @@ Proof.
   replace (Val.add (eval_addrmode32 ge addr rs1) (Vint Int.zero))
      with (eval_addrmode ge addr rs1).
   rewrite H0. eauto.
-  unfold eval_addrmode in *; rewrite H1 in *. 
+  unfold eval_addrmode in *; rewrite H1 in *.
   destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate.
   simpl. rewrite H1. rewrite Ptrofs.add_zero; auto.
   auto. auto. auto.
@@ -358,10 +358,10 @@ Remark eval_addrmode_indexed:
   match rs#base with Vptr _ _ => True | _ => False end ->
   eval_addrmode ge (Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs))) rs = Val.offset_ptr rs#base ofs.
 Proof.
-  intros. destruct (rs#base) eqn:BASE; try contradiction. 
+  intros. destruct (rs#base) eqn:BASE; try contradiction.
   intros; unfold eval_addrmode; destruct Archi.ptr64 eqn:SF; simpl; rewrite BASE; simpl; rewrite SF; simpl.
-- do 2 f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
-- do 2 f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
+- apply f_equal. apply f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
+-  apply f_equal. apply f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs.
 Qed.
 
 Ltac loadind_correct_solve :=
@@ -420,7 +420,7 @@ Lemma transl_addressing_mode_32_correct:
 Proof.
   assert (A: forall id ofs, Archi.ptr64 = false ->
           Val.add (Vint Int.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs).
-  { intros. unfold Val.add; rewrite H. unfold Genv.symbol_address. 
+  { intros. unfold Val.add; rewrite H. unfold Genv.symbol_address.
     destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. }
   assert (C: forall v i,
     Val.lessdef (Val.mul v (Vint (Int.repr i)))
@@ -440,7 +440,7 @@ Proof.
 - destruct Archi.ptr64 eqn:SF; inv H2. erewrite ireg_of_eq by eauto.
   rewrite Val.add_permut. rewrite Val.add_commut. apply Val.add_lessdef; auto. rewrite A; auto.
 - destruct Archi.ptr64 eqn:SF; inv H2. simpl.
-  destruct (rs RSP); simpl; auto; rewrite SF. 
+  destruct (rs RSP); simpl; auto; rewrite SF.
   rewrite Int.add_zero_l. apply Val.lessdef_same; f_equal; f_equal.
   symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints.
 Qed.
@@ -453,7 +453,7 @@ Lemma transl_addressing_mode_64_correct:
 Proof.
   assert (A: forall id ofs, Archi.ptr64 = true ->
           Val.addl (Vlong Int64.zero) (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs).
-  { intros. unfold Val.addl; rewrite H. unfold Genv.symbol_address. 
+  { intros. unfold Val.addl; rewrite H. unfold Genv.symbol_address.
     destruct (Genv.find_symbol ge id); auto. rewrite Ptrofs.add_zero; auto. }
   assert (C: forall v i,
     Val.lessdef (Val.mull v (Vlong (Int64.repr i)))
@@ -469,7 +469,7 @@ Proof.
 - apply Val.addl_lessdef; auto. apply Val.addl_lessdef; auto.
 - destruct Archi.ptr64 eqn:SF; inv H2. rewrite ! A by auto. auto.
 - destruct Archi.ptr64 eqn:SF; inv H2. simpl.
-  destruct (rs RSP); simpl; auto; rewrite SF. 
+  destruct (rs RSP); simpl; auto; rewrite SF.
   rewrite Int64.add_zero_l. apply Val.lessdef_same; f_equal; f_equal.
   symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints.
 Qed.
@@ -480,7 +480,7 @@ Lemma transl_addressing_mode_correct:
   eval_addressing ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v ->
   Val.lessdef v (eval_addrmode ge am rs).
 Proof.
-  unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64. 
+  unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64.
   eapply transl_addressing_mode_64_correct; eauto.
   eapply transl_addressing_mode_32_correct; eauto.
 Qed.
@@ -492,16 +492,16 @@ Proof.
 Qed.
 
 Lemma normalize_addrmode_64_correct:
-  forall am rs, 
+  forall am rs,
   eval_addrmode64 ge am rs =
   match normalize_addrmode_64 am with
   | (am', None) => eval_addrmode64 ge am' rs
   | (am', Some delta) => Val.addl (eval_addrmode64 ge am' rs) (Vlong delta)
   end.
 Proof.
-  intros; destruct am as [base ofs [n|r]]; simpl; auto. 
+  intros; destruct am as [base ofs [n|r]]; simpl; auto.
   destruct (zeq (Int.signed (Int.repr n)) n); simpl; auto.
-  rewrite ! Val.addl_assoc. do 2 f_equal. simpl. rewrite Int64.add_zero_l; auto.
+  rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto.
 Qed.
 
 (** Processor conditions and comparisons *)
@@ -657,7 +657,7 @@ Proof.
   intros. generalize (compare_longs_spec rs v1 v2 m).
   set (rs' := nextinstr (compare_longs v1 v2 rs m)).
   intros [A [B [C [D E]]]].
-  unfold eval_testcond. rewrite A; rewrite B. 
+  unfold eval_testcond. rewrite A; rewrite B.
   destruct v1; destruct v2; simpl in H; inv H.
 - (* int int *)
   destruct c; simpl; auto.
@@ -1365,11 +1365,11 @@ Transparent destroyed_by_op.
 (* leal *)
   exploit transl_addressing_mode_64_correct; eauto. intros EA.
   generalize (normalize_addrmode_64_correct x rs). destruct (normalize_addrmode_64 x) as [am' [delta|]]; intros EV.
-  econstructor; split. eapply exec_straight_two. 
-  simpl. reflexivity.  simpl. reflexivity. auto. auto. 
+  econstructor; split. eapply exec_straight_two.
+  simpl. reflexivity.  simpl. reflexivity. auto. auto.
   split. rewrite nextinstr_nf_inv by auto. rewrite Pregmap.gss. rewrite nextinstr_inv by auto with asmgen.
   rewrite Pregmap.gss. rewrite <- EV; auto.
-  intros; Simplifs. 
+  intros; Simplifs.
   TranslOp. rewrite nextinstr_inv; auto with asmgen. rewrite Pregmap.gss; auto. rewrite <- EV; auto.
 (* intoffloat *)
   apply SAME. TranslOp. rewrite H0; auto.
@@ -1475,5 +1475,3 @@ Proof.
 Qed.
 
 End CONSTRUCTORS.
-
-
diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v
index fced9a07..4cd15fd3 100644
--- a/ia32/SelectLongproof.v
+++ b/ia32/SelectLongproof.v
@@ -64,7 +64,7 @@ Proof.
   unfold longconst; intros; destruct Archi.splitlong.
   apply SplitLongproof.eval_longconst.
   EvalOp.
-Qed. 
+Qed.
 
 Lemma is_longconst_sound_1:
   forall a n, is_longconst a = Some n -> a = Eop (Olongconst n) Enil.
@@ -83,46 +83,46 @@ Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword.
 Proof.
   unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong.
   red; intros. destruct (is_longconst a) as [n|] eqn:C.
-- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto.  
-- TrivialExists. 
-Qed. 
+- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto.
+- TrivialExists.
+Qed.
 
 Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu.
 Proof.
   unfold longofintu; destruct Archi.splitlong. apply SplitLongproof.eval_longofintu.
   red; intros. destruct (is_intconst a) as [n|] eqn:C.
-- econstructor; split. apply eval_longconst. 
+- econstructor; split. apply eval_longconst.
   exploit is_intconst_sound; eauto. intros; subst x. auto.
-- TrivialExists. 
-Qed. 
+- TrivialExists.
+Qed.
 
 Theorem eval_longofint: unary_constructor_sound longofint Val.longofint.
 Proof.
   unfold longofint; destruct Archi.splitlong. apply SplitLongproof.eval_longofint.
   red; intros. destruct (is_intconst a) as [n|] eqn:C.
-- econstructor; split. apply eval_longconst. 
+- econstructor; split. apply eval_longconst.
   exploit is_intconst_sound; eauto. intros; subst x. auto.
-- TrivialExists. 
-Qed. 
+- TrivialExists.
+Qed.
 
 Theorem eval_notl: unary_constructor_sound notl Val.notl.
 Proof.
   unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl.
-  red; intros. destruct (notl_match a). 
+  red; intros. destruct (notl_match a).
 - InvEval. econstructor; split. apply eval_longconst. auto.
 - InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto.
-- TrivialExists. 
-Qed. 
+- TrivialExists.
+Qed.
 
 Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)).
 Proof.
-  unfold andlimm; intros; red; intros. 
+  unfold andlimm; intros; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
-  exists (Vlong Int64.zero); split. apply eval_longconst. 
-  subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto. 
+  exists (Vlong Int64.zero); split. apply eval_longconst.
+  subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone.
   exists x; split. assumption.
-  subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto. 
+  subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto.
   destruct (andlimm_match a); InvEval; subst.
 - econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto.
 - TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto.
@@ -131,7 +131,7 @@ Qed.
 
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
 Proof.
-  unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. 
+  unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl.
   red; intros. destruct (andl_match a b).
 - InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto.
 - InvEval. apply eval_andlimm; auto.
@@ -140,7 +140,7 @@ Qed.
 
 Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)).
 Proof.
-  unfold orlimm; intros; red; intros. 
+  unfold orlimm; intros; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.or_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone.
@@ -153,7 +153,7 @@ Qed.
 
 Theorem eval_orl: binary_constructor_sound orl Val.orl.
 Proof.
-  unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. 
+  unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
   red; intros.
   assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oorl (a:::b:::Enil)) v /\ Val.lessdef (Val.orl x y) v) by TrivialExists.
   assert (ROR: forall v n1 n2,
@@ -180,23 +180,24 @@ Qed.
 
 Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)).
 Proof.
-  unfold xorlimm; intros; red; intros. 
+  unfold xorlimm; intros; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   exists x; split; auto. subst. destruct x; simpl; auto. rewrite Int64.xor_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone.
   replace (Val.xorl x (Vlong n)) with (Val.notl x). apply eval_notl; auto.
-  subst n. destruct x; simpl; auto.  
+  subst n. destruct x; simpl; auto.
   destruct (xorlimm_match a); InvEval; subst.
 - econstructor; split. apply eval_longconst. simpl. rewrite Int64.xor_commut; auto.
 - TrivialExists. simpl. rewrite Val.xorl_assoc. rewrite Int64.xor_commut; auto.
 - TrivialExists. simpl. destruct v1; simpl; auto. unfold Int64.not.
-  rewrite Int64.xor_assoc. do 3 f_equal. apply Int64.xor_commut.       
+  rewrite Int64.xor_assoc. apply f_equal. apply f_equal. apply f_equal.
+  apply Int64.xor_commut.
 - TrivialExists.
 Qed.
 
 Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.
 Proof.
-  unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl. 
+  unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl.
   red; intros. destruct (xorl_match a b).
 - InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto.
 - InvEval. apply eval_xorlimm; auto.
@@ -305,19 +306,19 @@ Theorem eval_negl: unary_constructor_sound negl Val.negl.
 Proof.
   unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto.
   red; intros. destruct (is_longconst a) as [n|] eqn:C.
-- exploit is_longconst_sound; eauto. intros EQ; subst x. 
+- exploit is_longconst_sound; eauto. intros EQ; subst x.
   econstructor; split. apply eval_longconst. auto.
 - TrivialExists.
-Qed.    
+Qed.
 
 Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
 Proof.
-  unfold addlimm; intros; red; intros. 
+  unfold addlimm; intros; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   subst. exists x; split; auto.
   destruct x; simpl; auto.
   rewrite Int64.add_zero; auto.
-  destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. 
+  destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto.
   destruct (addlimm_match a); InvEval.
 - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
 - inv H. simpl in H6. TrivialExists. simpl.
@@ -332,10 +333,10 @@ Proof.
   assert (B: forall id ofs n, Archi.ptr64 = true ->
              Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) =
              Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))).
-  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs. 
+  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs.
     apply Genv.shift_symbol_address_64; auto. }
   unfold addl. destruct Archi.splitlong eqn:SL.
-  apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto. 
+  apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto.
   red; intros; destruct (addl_match a b); InvEval.
 - rewrite Val.addl_commut. apply eval_addlimm; auto.
 - apply eval_addlimm; auto.
@@ -373,7 +374,7 @@ Qed.
 
 Theorem eval_mullimm_base: forall n, unary_constructor_sound (mullimm_base n) (fun v => Val.mull v (Vlong n)).
 Proof.
-  intros; unfold mullimm_base. red; intros. 
+  intros; unfold mullimm_base. red; intros.
   generalize (Int64.one_bits'_decomp n); intros D.
   destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B.
 - TrivialExists.
@@ -416,7 +417,7 @@ Proof.
   rewrite (Int64.mul_commut n). auto.
   destruct Archi.ptr64; auto.
 - apply eval_mullimm_base; auto.
-Qed.     
+Qed.
 
 Theorem eval_mull: binary_constructor_sound mull Val.mull.
 Proof.
@@ -442,28 +443,28 @@ Proof.
 Qed.
 
 Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
-Proof. 
+Proof.
   unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divls_base; eauto.
   TrivialExists.
 Qed.
 
 Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls.
-Proof. 
+Proof.
   unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modls_base; eauto.
   TrivialExists.
 Qed.
-  
+
 Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu.
-Proof. 
+Proof.
   unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divlu_base; eauto.
   TrivialExists.
 Qed.
 
 Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu.
-Proof. 
+Proof.
   unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modlu_base; eauto.
   TrivialExists.
@@ -476,7 +477,7 @@ Theorem eval_cmplu:
   Val.cmplu (Mem.valid_pointer m) c x y = Some v ->
   eval_expr ge sp e m le (cmplu c a b) v.
 Proof.
-  unfold cmplu; intros. destruct Archi.splitlong eqn:SL. 
+  unfold cmplu; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_cmplu; eauto. apply Archi.splitlong_ptr32; auto.
   unfold Val.cmplu in H1.
   destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1.
@@ -497,7 +498,7 @@ Theorem eval_cmpl:
   Val.cmpl c x y = Some v ->
   eval_expr ge sp e m le (cmpl c a b) v.
 Proof.
-  unfold cmpl; intros. destruct Archi.splitlong eqn:SL. 
+  unfold cmpl; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_cmpl; eauto.
   unfold Val.cmpl in H1.
   destruct (Val.cmpl_bool c x y) as [vb|] eqn:C; simpl in H1; inv H1.
@@ -516,27 +517,27 @@ Proof.
   unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longoffloat; eauto.
   TrivialExists.
-Qed. 
+Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
 Proof.
   unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflong; eauto.
   TrivialExists.
-Qed. 
+Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
 Proof.
   unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longofsingle; eauto.
   TrivialExists.
-Qed. 
+Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
   unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_singleoflong; eauto.
   TrivialExists.
-Qed. 
+Qed.
 
 End CMCONSTR.