simpl -> cbn

1 files changed, 27 insertions, 27 deletions

diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index 4c354d5a..f636336d 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -229,7 +229,7 @@ Lemma needs_of_condition0_sound:
 Proof.
   intros until arg2.
   intros Hcond Hagree.
-  apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto.
+  apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); cbn; auto.
   apply val_inject_lessdef. apply lessdef_vagree. assumption.
 Qed.
 
@@ -239,7 +239,7 @@ Lemma addl_sound:
   vagree (Val.addl v1 v2) (Val.addl w1 w2) x.
 Proof.
   unfold default; intros.
-  destruct x; simpl in *; trivial.
+  destruct x; cbn in *; trivial.
   - unfold Val.addl.
     destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial.
   - apply Val.addl_lessdef; trivial.
@@ -249,7 +249,7 @@ Lemma subl_lessdef:
   forall v1 v1' v2 v2',
   Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2').
 Proof.
-  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+  intros. inv H. inv H0. auto. destruct v1'; cbn; auto. cbn; auto.
 Qed.
 
 Lemma subl_sound:
@@ -258,10 +258,10 @@ Lemma subl_sound:
   vagree (Val.subl v1 v2) (Val.subl w1 w2) x.
 Proof.
   unfold default; intros.
-  destruct x; simpl in *; trivial.
+  destruct x; cbn in *; trivial.
   - unfold Val.subl.
-    destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial.
-    destruct (eq_block _ _) ; simpl; trivial.
+    destruct v1; destruct v2; trivial; destruct Archi.ptr64; cbn; trivial.
+    destruct (eq_block _ _) ; cbn; trivial.
   - apply subl_lessdef; trivial.
 Qed.
 
@@ -272,7 +272,7 @@ Lemma mull_sound:
   vagree (Val.mull v1 v2) (Val.mull w1 w2) x.
 Proof.
   unfold default; intros.
-  destruct x; simpl in *; trivial.
+  destruct x; cbn in *; trivial.
   - unfold Val.mull.
     destruct v1; destruct v2; trivial.
   - unfold Val.mull.
@@ -284,7 +284,7 @@ Qed.
 
 Remark default_idem: forall nv, default (default nv) = default nv.
 Proof.
-  destruct nv; simpl; trivial.
+  destruct nv; cbn; trivial.
 Qed.
 
 Lemma vagree_triple_op_float :
@@ -298,14 +298,14 @@ Proof.
   induction nv;
   intros Hax Hby Hcz.
   - trivial.
-  - simpl in *. destruct a; simpl; trivial.
-    destruct b; simpl; trivial.
-    destruct c; simpl; trivial.
-  - simpl in *. destruct a; simpl; trivial.
-    destruct b; simpl; trivial.
-    destruct c; simpl; trivial.
+  - cbn in *. destruct a; cbn; trivial.
+    destruct b; cbn; trivial.
+    destruct c; cbn; trivial.
+  - cbn in *. destruct a; cbn; trivial.
+    destruct b; cbn; trivial.
+    destruct c; cbn; trivial.
     inv Hax. inv Hby. inv Hcz.
-    simpl.
+    cbn.
     constructor.
 Qed.
 
@@ -320,14 +320,14 @@ Proof.
   induction nv;
   intros Hax Hby Hcz.
   - trivial.
-  - simpl in *. destruct a; simpl; trivial.
-    destruct b; simpl; trivial.
-    destruct c; simpl; trivial.
-  - simpl in *. destruct a; simpl; trivial.
-    destruct b; simpl; trivial.
-    destruct c; simpl; trivial.
+  - cbn in *. destruct a; cbn; trivial.
+    destruct b; cbn; trivial.
+    destruct c; cbn; trivial.
+  - cbn in *. destruct a; cbn; trivial.
+    destruct b; cbn; trivial.
+    destruct c; cbn; trivial.
     inv Hax. inv Hby. inv Hcz.
-    simpl.
+    cbn.
     constructor.
 Qed.
 
@@ -343,7 +343,7 @@ Lemma needs_of_operation_sound:
   /\ vagree v v' nv.
 Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
-  simpl in *; FuncInv; InvAgree; TrivialExists.
+  cbn in *; FuncInv; InvAgree; TrivialExists.
 - apply sign_ext_sound; auto. compute; auto. 
 - apply sign_ext_sound; auto. compute; auto. 
 - apply add_sound; auto.
@@ -384,17 +384,17 @@ Proof.
 - destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
   erewrite needs_of_condition0_sound by eauto.
   apply select_sound; auto.
-  simpl; auto with na.
+  cbn; auto with na.
   (* select imm *)
 - destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
   { erewrite needs_of_condition0_sound by eauto.
   apply select_sound; auto with na. }
-  simpl; auto with na.
+  cbn; auto with na.
   (* select long imm *)
 - destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
   { erewrite needs_of_condition0_sound by eauto.
   apply select_sound; auto with na. }
-  simpl; auto with na.
+  cbn; auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
@@ -404,7 +404,7 @@ Lemma operation_is_redundant_sound:
   vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) ->
   vagree v arg1' nv.
 Proof.
-  intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
+  intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst.
 - apply sign_ext_redundant_sound; auto. omega.
 - apply sign_ext_redundant_sound; auto. omega.
 - apply andimm_redundant_sound; auto.