simpl -> cbn

1 files changed, 98 insertions, 98 deletions

diff --git a/kvx/ConstpropOpproof.v b/kvx/ConstpropOpproof.v
index 05bbdde1..ffd35bcc 100644
--- a/kvx/ConstpropOpproof.v
+++ b/kvx/ConstpropOpproof.v
@@ -105,7 +105,7 @@ Proof.
   + (* global *)
     inv H2. exists (Genv.symbol_address ge id ofs); auto.
   + (* stack *)
-    inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto.
+    inv H2. exists (Vptr sp ofs); split; auto. cbn. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma cond_strength_reduction_correct:
@@ -115,7 +115,7 @@ Lemma cond_strength_reduction_correct:
   eval_condition cond' e##args' m = eval_condition cond e##args m.
 Proof.
   intros until vl. unfold cond_strength_reduction.
-  case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM.
+  case (cond_strength_reduction_match cond args vl); cbn; intros; InvApproxRegs; SimplVM.
 - apply Val.swap_cmp_bool.
 - auto.
 - apply Val.swap_cmpu_bool.
@@ -137,7 +137,7 @@ Proof.
   intros. unfold make_cmp_base.
   generalize (cond_strength_reduction_correct c args vl H).
   destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ.
-  econstructor; split. simpl; eauto. rewrite EQ. auto.
+  econstructor; split. cbn; eauto. rewrite EQ. auto.
 Qed.
 
 Lemma make_cmp_correct:
@@ -154,43 +154,43 @@ Proof.
   unfold make_cmp. case (make_cmp_match c args vl); intros.
 - unfold make_cmp_imm_eq.
   destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-+ simpl in H; inv H. InvBooleans. subst n.
-  exists (e#r1); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ cbn in H; inv H. InvBooleans. subst n.
+  exists (e#r1); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-* simpl in H; inv H. InvBooleans. subst n.
-  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* cbn in H; inv H. InvBooleans. subst n.
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 * apply make_cmp_base_correct; auto.
 - unfold make_cmp_imm_ne.
   destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-+ simpl in H; inv H. InvBooleans. subst n.
-  exists (e#r1); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ cbn in H; inv H. InvBooleans. subst n.
+  exists (e#r1); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-* simpl in H; inv H. InvBooleans. subst n.
-  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* cbn in H; inv H. InvBooleans. subst n.
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 * apply make_cmp_base_correct; auto.
 - unfold make_cmp_imm_eq.
   destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-+ simpl in H; inv H. InvBooleans. subst n.
-  exists (e#r1); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ cbn in H; inv H. InvBooleans. subst n.
+  exists (e#r1); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-* simpl in H; inv H. InvBooleans. subst n.
-  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* cbn in H; inv H. InvBooleans. subst n.
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 * apply make_cmp_base_correct; auto.
 - unfold make_cmp_imm_ne.
   destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0.
-+ simpl in H; inv H. InvBooleans. subst n.
-  exists (e#r1); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
++ cbn in H; inv H. InvBooleans. subst n.
+  exists (e#r1); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1.
-* simpl in H; inv H. InvBooleans. subst n.
-  exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl.
-  exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto.
+* cbn in H; inv H. InvBooleans. subst n.
+  exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn.
+  exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto.
 * apply make_cmp_base_correct; auto.
 - apply make_cmp_base_correct; auto.
 Qed.
@@ -203,7 +203,7 @@ Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (e#r); split; auto.
-  destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
+  destruct (e#r); cbn; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
   exists (Val.add e#r (Vint n)); split; auto.
 Qed.
 
@@ -215,10 +215,10 @@ Lemma make_shlimm_correct:
 Proof.
   intros; unfold make_shlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shl_zero. auto.
   destruct (Int.ltu n Int.iwordsize).
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shrimm_correct:
@@ -229,10 +229,10 @@ Lemma make_shrimm_correct:
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shr_zero. auto.
   destruct (Int.ltu n Int.iwordsize).
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shruimm_correct:
@@ -243,10 +243,10 @@ Lemma make_shruimm_correct:
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shru_zero. auto.
   destruct (Int.ltu n Int.iwordsize).
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_mulimm_correct:
@@ -257,12 +257,12 @@ Lemma make_mulimm_correct:
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto.
+  exists (Vint Int.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_one; auto.
   destruct (Int.is_power2 n) eqn:?; intros.
-  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto.
-  econstructor; split; eauto. simpl. rewrite H; auto.
+  rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. cbn; eauto. auto.
+  econstructor; split; eauto. cbn. rewrite H; auto.
 Qed.
 
 Lemma make_divimm_correct:
@@ -275,11 +275,11 @@ Proof.
   intros; unfold make_divimm.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
   destruct (e#r1) eqn:?;
-    try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
+    try (rewrite Val.divs_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto);
     inv H; auto.
   destruct (Int.is_power2 n) eqn:?.
   destruct (Int.ltu i (Int.repr 31)) eqn:?.
-  exists v; split; auto. simpl.
+  exists v; split; auto. cbn.
   erewrite Val.divs_pow2; eauto. reflexivity. congruence.
   exists v; auto.
   exists v; auto.
@@ -295,10 +295,10 @@ Proof.
   intros; unfold make_divuimm.
   predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
   destruct (e#r1) eqn:?;
-    try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
+    try (rewrite Val.divu_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto);
     inv H; auto.
   destruct (Int.is_power2 n) eqn:?.
-  econstructor; split. simpl; eauto.
+  econstructor; split. cbn; eauto.
   rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
   exists v; auto.
 Qed.
@@ -312,7 +312,7 @@ Lemma make_moduimm_correct:
 Proof.
   intros; unfold make_moduimm.
   destruct (Int.is_power2 n) eqn:?.
-  exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence.
+  exists v; split; auto. cbn. decEq. eapply Val.modu_pow2; eauto. congruence.
   exists v; auto.
 Qed.
 
@@ -324,18 +324,18 @@ Lemma make_andimm_correct:
 Proof.
   intros; unfold make_andimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto.
+  subst n. exists (Vint Int.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_mone; auto.
   destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero
                        | _ => false end) eqn:UNS.
   destruct x; try congruence.
   exists (e#r); split; auto.
-  inv H; auto. simpl. replace (Int.and i n) with i; auto.
+  inv H; auto. cbn. replace (Int.and i n) with i; auto.
   generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
-  rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
+  rewrite Int.bits_zero. cbn. rewrite andb_true_r. auto.
   rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
@@ -349,9 +349,9 @@ Lemma make_orimm_correct:
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
-  subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto.
+  subst n. exists (Vint Int.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_mone; auto.
   econstructor; split; eauto. auto.
 Qed.
 
@@ -362,7 +362,7 @@ Lemma make_xorimm_correct:
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.xor_zero; auto.
   predSpec Int.eq Int.eq_spec n Int.mone; intros.
   subst n. exists (Val.notint e#r); split; auto.
   econstructor; split; eauto. auto.
@@ -376,7 +376,7 @@ Proof.
   intros. unfold make_addlimm.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
   subst. exists (e#r); split; auto.
-  destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
+  destruct (e#r); cbn; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
   exists (Val.addl e#r (Vlong n)); split; auto.
 Qed.
 
@@ -388,11 +388,11 @@ Lemma make_shllimm_correct:
 Proof.
   intros; unfold make_shllimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto.
   unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto.
   destruct (Int.ltu n Int64.iwordsize').
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shrlimm_correct:
@@ -403,11 +403,11 @@ Lemma make_shrlimm_correct:
 Proof.
   intros; unfold make_shrlimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto.
   unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto.
   destruct (Int.ltu n Int64.iwordsize').
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_shrluimm_correct:
@@ -418,11 +418,11 @@ Lemma make_shrluimm_correct:
 Proof.
   intros; unfold make_shrluimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto.
   unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto.
   destruct (Int.ltu n Int64.iwordsize').
-  econstructor; split. simpl. eauto. auto.
-  econstructor; split. simpl. eauto. rewrite H; auto.
+  econstructor; split. cbn. eauto. auto.
+  econstructor; split. cbn. eauto. rewrite H; auto.
 Qed.
 
 Lemma make_mullimm_correct:
@@ -433,15 +433,15 @@ Lemma make_mullimm_correct:
 Proof.
   intros; unfold make_mullimm.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst.
-  exists (Vlong Int64.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_zero; auto.
+  exists (Vlong Int64.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst.
-  exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_one; auto.
+  exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_one; auto.
   destruct (Int64.is_power2' n) eqn:?; intros.
   exists (Val.shll e#r1 (Vint i)); split; auto.
-  destruct (e#r1); simpl; auto.
+  destruct (e#r1); cbn; auto.
   erewrite Int64.is_power2'_range by eauto.
   erewrite Int64.mul_pow2' by eauto. auto.
-  econstructor; split; eauto. simpl; rewrite H; auto.
+  econstructor; split; eauto. cbn; rewrite H; auto.
 Qed.
 
 Lemma make_divlimm_correct:
@@ -453,7 +453,7 @@ Lemma make_divlimm_correct:
 Proof.
   intros; unfold make_divlimm.
   destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?.
-  rewrite H0 in H. econstructor; split. simpl; eauto.
+  rewrite H0 in H. econstructor; split. cbn; eauto.
   erewrite Val.divls_pow2; eauto. auto.
   exists v; auto.
   exists v; auto.
@@ -468,9 +468,9 @@ Lemma make_divluimm_correct:
 Proof.
   intros; unfold make_divluimm.
   destruct (Int64.is_power2' n) eqn:?.
-  econstructor; split. simpl; eauto.
+  econstructor; split. cbn; eauto.
   rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
-  simpl.
+  cbn.
   erewrite Int64.is_power2'_range by eauto.    
   erewrite Int64.divu_pow2' by eauto.  auto. 
   exists v; auto.
@@ -485,9 +485,9 @@ Lemma make_modluimm_correct:
 Proof.
   intros; unfold make_modluimm.
   destruct (Int64.is_power2 n) eqn:?.
-  exists v; split; auto. simpl. decEq.
+  exists v; split; auto. cbn. decEq.
   rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. 
-  simpl. erewrite Int64.modu_and by eauto. auto.
+  cbn. erewrite Int64.modu_and by eauto. auto.
   exists v; auto.
 Qed.
 
@@ -498,9 +498,9 @@ Lemma make_andlimm_correct:
 Proof.
   intros; unfold make_andlimm.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
-  subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_zero; auto.
+  subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_mone; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_mone; auto.
   econstructor; split; eauto. auto.
 Qed.
 
@@ -511,9 +511,9 @@ Lemma make_orlimm_correct:
 Proof.
   intros; unfold make_orlimm.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
-  subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_mone; auto.
+  subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_mone; auto.
   econstructor; split; eauto. auto.
 Qed.
 
@@ -524,7 +524,7 @@ Lemma make_xorlimm_correct:
 Proof.
   intros; unfold make_xorlimm.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
-  subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.xor_zero; auto.
+  subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.xor_zero; auto.
   predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
   subst n. exists (Val.notl e#r); split; auto.
   econstructor; split; eauto. auto.
@@ -538,9 +538,9 @@ Lemma make_mulfimm_correct:
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
-  simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto.
-  simpl. econstructor; split; eauto.
+  cbn. econstructor; split. eauto. rewrite H; subst n.
+  destruct (e#r1); cbn; auto. rewrite Float.mul2_add; auto.
+  cbn. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfimm_correct_2:
@@ -551,10 +551,10 @@ Lemma make_mulfimm_correct_2:
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
-  simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto.
+  cbn. econstructor; split. eauto. rewrite H; subst n.
+  destruct (e#r2); cbn; auto. rewrite Float.mul2_add; auto.
   rewrite Float.mul_commut; auto.
-  simpl. econstructor; split; eauto.
+  cbn. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct:
@@ -565,9 +565,9 @@ Lemma make_mulfsimm_correct:
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
-  simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (e#r1); simpl; auto. rewrite Float32.mul2_add; auto.
-  simpl. econstructor; split; eauto.
+  cbn. econstructor; split. eauto. rewrite H; subst n.
+  destruct (e#r1); cbn; auto. rewrite Float32.mul2_add; auto.
+  cbn. econstructor; split; eauto.
 Qed.
 
 Lemma make_mulfsimm_correct_2:
@@ -578,10 +578,10 @@ Lemma make_mulfsimm_correct_2:
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
-  simpl. econstructor; split. eauto. rewrite H; subst n.
-  destruct (e#r2); simpl; auto. rewrite Float32.mul2_add; auto.
+  cbn. econstructor; split. eauto. rewrite H; subst n.
+  destruct (e#r2); cbn; auto. rewrite Float32.mul2_add; auto.
   rewrite Float32.mul_commut; auto.
-  simpl. econstructor; split; eauto.
+  cbn. econstructor; split; eauto.
 Qed.
 
 Lemma make_cast8signed_correct:
@@ -594,8 +594,8 @@ Proof.
   exists e#r; split; auto.
   assert (V: vmatch bc e#r (Sgn Ptop 8)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
-  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
-  econstructor; split; simpl; eauto.
+  inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
+  econstructor; split; cbn; eauto.
 Qed.
 
 Lemma make_cast16signed_correct:
@@ -608,8 +608,8 @@ Proof.
   exists e#r; split; auto.
   assert (V: vmatch bc e#r (Sgn Ptop 16)).
   { eapply vmatch_ge; eauto. apply vincl_ge; auto. }
-  inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
-  econstructor; split; simpl; eauto.
+  inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto.
+  econstructor; split; cbn; eauto.
 Qed.
 
 Lemma op_strength_reduction_correct:
@@ -620,7 +620,7 @@ Lemma op_strength_reduction_correct:
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some w /\ Val.lessdef v w.
 Proof.
   intros until v; unfold op_strength_reduction;
-  case (op_strength_reduction_match op args vl); simpl; intros.
+  case (op_strength_reduction_match op args vl); cbn; intros.
 - (* cast8signed *)
   InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto.
 - (* cast16signed *)
@@ -733,15 +733,15 @@ Lemma addr_strength_reduction_correct:
   exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'.
 Proof.
   intros until res. unfold addr_strength_reduction.
-  destruct (addr_strength_reduction_match addr args vl); simpl;
+  destruct (addr_strength_reduction_match addr args vl); cbn;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
 - destruct (orb _ _).
 + exists (Val.offset_ptr e#r1 n); auto.
-+ simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
-  inv H0; simpl; auto.
++ cbn. rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
+  inv H0; cbn; auto.
 - rewrite Ptrofs.add_zero_l. econstructor; split; eauto.
   change (Vptr sp (Ptrofs.add n1 n)) with (Val.offset_ptr (Vptr sp n1) n). 
-  inv H0; simpl; auto.
+  inv H0; cbn; auto.
 - exists res; auto.
 Qed.