simpl -> cbn

1 files changed, 28 insertions, 28 deletions

diff --git a/kvx/CombineOpproof.v b/kvx/CombineOpproof.v
index dafc90df..5dffc565 100644
--- a/kvx/CombineOpproof.v
+++ b/kvx/CombineOpproof.v
@@ -46,7 +46,7 @@ Qed.
 Ltac UseGetSound :=
   match goal with
   | [ H: get _ = Some _ |- _ ] =>
-      let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
+      let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; cbn in x; FuncInv)
   end.
 
 Lemma combine_compimm_ne_0_sound:
@@ -58,7 +58,7 @@ Proof.
   intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
   (* of cmp *)
   UseGetSound. rewrite <- H.
-  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  destruct (eval_condition cond (map valu args) m); cbn; auto. destruct b; auto.
 Qed.
 
 Lemma combine_compimm_eq_0_sound:
@@ -71,7 +71,7 @@ Proof.
   (* of cmp *)
   UseGetSound. rewrite <- H.
   rewrite eval_negate_condition.
-  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  destruct (eval_condition c (map valu args) m); cbn; auto. destruct b; auto.
 Qed.
 
 Lemma combine_compimm_eq_1_sound:
@@ -83,7 +83,7 @@ Proof.
   intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ.
   (* of cmp *)
   UseGetSound. rewrite <- H.
-  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+  destruct (eval_condition cond (map valu args) m); cbn; auto. destruct b; auto.
 Qed.
 
 Lemma combine_compimm_ne_1_sound:
@@ -96,7 +96,7 @@ Proof.
   (* of cmp *)
   UseGetSound. rewrite <- H.
   rewrite eval_negate_condition.
-  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+  destruct (eval_condition c (map valu args) m); cbn; auto. destruct b; auto.
 Qed.
 
 Theorem combine_cond_sound:
@@ -106,21 +106,21 @@ Theorem combine_cond_sound:
 Proof.
   intros. functional inversion H; subst.
   (* compimm ne zero *)
-  - simpl; eapply combine_compimm_ne_0_sound; eauto.
+  - cbn; eapply combine_compimm_ne_0_sound; eauto.
   (* compimm ne one *)
-  - simpl; eapply combine_compimm_ne_1_sound; eauto.
+  - cbn; eapply combine_compimm_ne_1_sound; eauto.
   (* compimm eq zero *)
-  - simpl; eapply combine_compimm_eq_0_sound; eauto.
+  - cbn; eapply combine_compimm_eq_0_sound; eauto.
   (* compimm eq one *)
-  - simpl; eapply combine_compimm_eq_1_sound; eauto.
+  - cbn; eapply combine_compimm_eq_1_sound; eauto.
   (* compuimm ne zero *)
-  - simpl; eapply combine_compimm_ne_0_sound; eauto.
+  - cbn; eapply combine_compimm_ne_0_sound; eauto.
   (* compuimm ne one *)
-  - simpl; eapply combine_compimm_ne_1_sound; eauto.
+  - cbn; eapply combine_compimm_ne_1_sound; eauto.
   (* compuimm eq zero *)
-  - simpl; eapply combine_compimm_eq_0_sound; eauto.
+  - cbn; eapply combine_compimm_eq_0_sound; eauto.
   (* compuimm eq one *)
-  - simpl; eapply combine_compimm_eq_1_sound; eauto.
+  - cbn; eapply combine_compimm_eq_1_sound; eauto.
 Qed.
 
 Theorem combine_addr_sound:
@@ -130,10 +130,10 @@ Theorem combine_addr_sound:
 Proof.
   intros. functional inversion H; subst.
 - (* indexed - addimm *)
-  UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl.
+  UseGetSound. cbn. rewrite <- H0. destruct v; auto. cbn; rewrite H7; cbn.
   rewrite Ptrofs.add_assoc. auto.
 - (* indexed - addimml *)
-  UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl.
+  UseGetSound. cbn. rewrite <- H0. destruct v; auto. cbn; rewrite H7; cbn.
   rewrite Ptrofs.add_assoc. auto.
 Qed.
 
@@ -144,33 +144,33 @@ Theorem combine_op_sound:
 Proof.
   intros. functional inversion H; subst.
   (* addimm - addimm *)
-  - UseGetSound. FuncInv. simpl.
+  - UseGetSound. FuncInv. cbn.
     rewrite <- H0. rewrite Val.add_assoc. auto.
   (* andimm - andimm *)
-  - UseGetSound; simpl.
+  - UseGetSound; cbn.
     generalize (Int.eq_spec p m0); rewrite H7; intros.
-    rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
-  - UseGetSound; simpl.
+    rewrite <- H0. rewrite Val.and_assoc. cbn. fold p. rewrite H1. auto.
+  - UseGetSound; cbn.
     rewrite <- H0. rewrite Val.and_assoc. auto.
   (* orimm - orimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
+  - UseGetSound. cbn. rewrite <- H0. rewrite Val.or_assoc. auto.
   (* xorimm - xorimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
+  - UseGetSound. cbn. rewrite <- H0. rewrite Val.xor_assoc. auto.
   (* addlimm - addlimm *)
-  - UseGetSound. FuncInv. simpl.
+  - UseGetSound. FuncInv. cbn.
     rewrite <- H0. rewrite Val.addl_assoc. auto.
   (* andlimm - andlimm *)
-  - UseGetSound; simpl.
+  - UseGetSound; cbn.
     generalize (Int64.eq_spec p m0); rewrite H7; intros.
-    rewrite <- H0. rewrite Val.andl_assoc. simpl. fold p. rewrite H1. auto.
-  - UseGetSound; simpl.
+    rewrite <- H0. rewrite Val.andl_assoc. cbn. fold p. rewrite H1. auto.
+  - UseGetSound; cbn.
     rewrite <- H0. rewrite Val.andl_assoc. auto.
   (* orlimm - orlimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.orl_assoc. auto.
+  - UseGetSound. cbn. rewrite <- H0. rewrite Val.orl_assoc. auto.
   (* xorlimm - xorlimm *)
-  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto.
+  - UseGetSound. cbn. rewrite <- H0. rewrite Val.xorl_assoc. auto.
   (* cmp *)
-  - simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+  - cbn. decEq; decEq. eapply combine_cond_sound; eauto.
 Qed.
 
 End COMBINE.