simpl -> cbn

1 files changed, 38 insertions, 38 deletions

diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v
index e634fdc0..122c9a60 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -406,8 +406,8 @@ Lemma intoffloat_total_sound:
     vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x).
 Proof.
   unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -420,8 +420,8 @@ Lemma intuoffloat_total_sound:
     vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x).
 Proof.
   unfold Val.intoffloat, intoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -434,8 +434,8 @@ Lemma intofsingle_total_sound:
     vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x).
 Proof.
   unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float32.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -448,8 +448,8 @@ Lemma intuofsingle_total_sound:
     vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x).
 Proof.
   unfold Val.intofsingle, intofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float32.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -461,7 +461,7 @@ Lemma singleofint_total_sound:
               vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x).
 Proof.
   unfold Val.singleofint, singleofint; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -474,7 +474,7 @@ Lemma singleofintu_total_sound:
               vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x).
 Proof.
   unfold Val.singleofintu, singleofintu; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -488,8 +488,8 @@ Lemma longoffloat_total_sound:
     vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x).
 Proof.
   unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -502,8 +502,8 @@ Lemma longuoffloat_total_sound:
     vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x).
 Proof.
   unfold Val.longoffloat, longoffloat_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -516,8 +516,8 @@ Lemma longofsingle_total_sound:
     vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x).
 Proof.
   unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float32.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -530,8 +530,8 @@ Lemma longuofsingle_total_sound:
     vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x).
 Proof.
   unfold Val.longofsingle, longofsingle_total. intros.
-  inv MATCH; simpl in *; try constructor.
-  all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor].
+  inv MATCH; cbn in *; try constructor.
+  all: destruct (Float32.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor].
   unfold ntop1, provenance.
   destruct (va_strict tt); constructor.
 Qed.
@@ -543,7 +543,7 @@ Lemma singleoflong_total_sound:
               vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x).
 Proof.
   unfold Val.singleoflong, singleoflong; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -556,7 +556,7 @@ Lemma singleoflongu_total_sound:
               vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x).
 Proof.
   unfold Val.singleoflongu, singleoflongu; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -569,7 +569,7 @@ Lemma floatoflong_total_sound:
               vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x).
 Proof.
   unfold Val.floatoflong, floatoflong; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -582,7 +582,7 @@ Lemma floatoflongu_total_sound:
               vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x).
 Proof.
   unfold Val.floatoflongu, floatoflongu; intros.
-  inv H; simpl.
+  inv H; cbn.
   all: auto with va.
   all: unfold ntop1, provenance.
   all: try constructor.
@@ -620,7 +620,7 @@ Proof.
   intros v x;
   intro MATCH;
   inversion MATCH;
-  simpl;
+  cbn;
   constructor.
 Qed.
 
@@ -632,9 +632,9 @@ Lemma triple_op_float_sound:
 Proof.
   intros until z.
   intros Hax Hby Hcz.
-  inv Hax; simpl; try constructor;
-  inv Hby; simpl; try constructor;
-  inv Hcz; simpl; try constructor.
+  inv Hax; cbn; try constructor;
+  inv Hby; cbn; try constructor;
+  inv Hcz; cbn; try constructor.
 Qed.
 
 Lemma triple_op_single_sound:
@@ -645,9 +645,9 @@ Lemma triple_op_single_sound:
 Proof.
   intros until z.
   intros Hax Hby Hcz.
-  inv Hax; simpl; try constructor;
-  inv Hby; simpl; try constructor;
-  inv Hcz; simpl; try constructor.
+  inv Hax; cbn; try constructor;
+  inv Hby; cbn; try constructor;
+  inv Hcz; cbn; try constructor.
 Qed.
 
 Lemma fmaddf_sound :
@@ -691,9 +691,9 @@ Proof.
   intros until aargs; intros VM. inv VM.
   destruct cond; auto with va.
   inv H0.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
   inv H2.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
   destruct cond; auto with va.
 Qed.
 
@@ -703,7 +703,7 @@ Theorem eval_static_condition0_sound:
   cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg).
 Proof.
   intros until aarg; intro VM.
-  destruct cond; simpl; eauto with va.
+  destruct cond; cbn; eauto with va.
 Qed.
 
 Lemma symbol_address_sound:
@@ -812,8 +812,8 @@ Proof.
     + eauto with va.
     + destruct n; destruct shift; reflexivity.
   - (* shrx *)
-    inv H1; simpl; try constructor.
-    all: destruct Int.ltu; [simpl | constructor; fail].
+    inv H1; cbn; try constructor.
+    all: destruct Int.ltu; [cbn | constructor; fail].
     all: auto with va.
   - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
     | Vlong n2 => Vlong (Int64.add n n2)
@@ -833,8 +833,8 @@ Proof.
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
   - (* shrxl *)
-    inv H1; simpl; try constructor.
-    all: destruct Int.ltu; [simpl | constructor; fail].
+    inv H1; cbn; try constructor.
+    all: destruct Int.ltu; [cbn | constructor; fail].
     all: auto with va.
   - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 
@@ -865,12 +865,12 @@ Proof.
   (* insf *)
   - unfold insf, eval_static_insf.
     destruct (is_bitfield _ _).
-    + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor.
+    + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor.
     + constructor.
   (* insfl *)
   - unfold insfl, eval_static_insfl.
     destruct (is_bitfieldl _ _).
-    + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor.
+    + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor.
     + constructor.
     (* select *)
   - apply select_sound; auto. eapply eval_static_condition0_sound; eauto.