simpl -> cbn

1 files changed, 36 insertions, 36 deletions

diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index 3664c00a..a0c10ddd 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -62,10 +62,10 @@ Lemma shift1_4_of_z_correct :
     end.
 Proof.
   intro. unfold shift1_4_of_z.
-  destruct (Z.eq_dec _ _); simpl; try congruence.
-  destruct (Z.eq_dec _ _); simpl; try congruence.
-  destruct (Z.eq_dec _ _); simpl; try congruence.
-  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); cbn; try congruence.
+  destruct (Z.eq_dec _ _); cbn; try congruence.
+  destruct (Z.eq_dec _ _); cbn; try congruence.
+  destruct (Z.eq_dec _ _); cbn; try congruence.
   trivial.
 Qed.
 
@@ -215,19 +215,19 @@ Theorem divu_is_divlu: forall v1 v2 : val,
     end.
 Proof.
   intros.
-  destruct v1; simpl; trivial.
-  destruct v2; simpl; trivial.
+  destruct v1; cbn; trivial.
+  destruct v2; cbn; trivial.
   destruct i as [i_val i_range].
   destruct i0 as [i0_val i0_range].
-  simpl.
+  cbn.
   unfold Int.eq, Int64.eq, Int.zero, Int64.zero.
-  simpl.
+  cbn.
   rewrite Int.unsigned_repr by (compute; split; discriminate).
   rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate).
   rewrite (unsigned64_repr i0_val) by assumption.
-  destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial.
+  destruct (zeq i0_val 0) as [ | Hnot0]; cbn; trivial.
   f_equal. f_equal.
-  unfold Int.divu, Int64.divu. simpl.
+  unfold Int.divu, Int64.divu. cbn.
   rewrite (unsigned64_repr i_val) by assumption.
   rewrite (unsigned64_repr i0_val) by assumption.
   unfold Int64.loword.
@@ -260,19 +260,19 @@ Theorem modu_is_modlu: forall v1 v2 : val,
     end.
 Proof.
   intros.
-  destruct v1; simpl; trivial.
-  destruct v2; simpl; trivial.
+  destruct v1; cbn; trivial.
+  destruct v2; cbn; trivial.
   destruct i as [i_val i_range].
   destruct i0 as [i0_val i0_range].
-  simpl.
+  cbn.
   unfold Int.eq, Int64.eq, Int.zero, Int64.zero.
-  simpl.
+  cbn.
   rewrite Int.unsigned_repr by (compute; split; discriminate).
   rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate).
   rewrite (unsigned64_repr i0_val) by assumption.
-  destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial.
+  destruct (zeq i0_val 0) as [ | Hnot0]; cbn; trivial.
   f_equal. f_equal.
-  unfold Int.modu, Int64.modu. simpl.
+  unfold Int.modu, Int64.modu. cbn.
   rewrite (unsigned64_repr i_val) by assumption.
   rewrite (unsigned64_repr i0_val) by assumption.
   unfold Int64.loword.
@@ -347,19 +347,19 @@ Theorem divs_is_divls: forall v1 v2 : val,
     end.
 Proof.
   intros.
-  destruct v1; simpl; trivial.
-  destruct v2; simpl; trivial.
+  destruct v1; cbn; trivial.
+  destruct v2; cbn; trivial.
   destruct i as [i_val i_range].
   destruct i0 as [i0_val i0_range].
-  simpl.
+  cbn.
   unfold Int.eq, Int64.eq, Int.zero, Int64.zero.
-  simpl.
+  cbn.
   replace (Int.unsigned (Int.repr 0)) with 0 in * by reflexivity.
-  destruct (zeq _ _) as [H0' | Hnot0]; simpl; trivial.
-  destruct (zeq i_val (Int.unsigned (Int.repr Int.min_signed))) as [Hmin | Hnotmin]; simpl.
+  destruct (zeq _ _) as [H0' | Hnot0]; cbn; trivial.
+  destruct (zeq i_val (Int.unsigned (Int.repr Int.min_signed))) as [Hmin | Hnotmin]; cbn.
   { subst.
     destruct (zeq i0_val (Int.unsigned Int.mone)) as [Hmone | Hnotmone]; trivial.
-    unfold Int.signed. simpl.
+    unfold Int.signed. cbn.
     replace (Int64.unsigned (Int64.repr 0)) with 0 in * by reflexivity.
     rewrite if_zlt_min_signed_half_modulus.
     replace (if
@@ -370,7 +370,7 @@ Proof.
              (Int64.unsigned (Int64.repr Int64.min_signed))
           then true
               else false) with false by reflexivity.
-    simpl.
+    cbn.
     rewrite orb_false_r.
     destruct (zlt i0_val Int.half_modulus) as [Hlt_half | Hge_half].
     {
@@ -380,7 +380,7 @@ Proof.
       unfold Val.loword.
       f_equal.
       unfold Int64.divs, Int.divs, Int64.loword.
-      unfold Int.signed, Int64.signed. simpl.      
+      unfold Int.signed, Int64.signed. cbn.      
       rewrite if_zlt_min_signed_half_modulus.
       change Int.half_modulus with 2147483648 in *.
       destruct (zlt _ _) as [discard|]; try omega. clear discard.
@@ -390,7 +390,7 @@ Proof.
       with 18446744071562067968.
       change Int64.half_modulus with 9223372036854775808.
       change Int64.modulus with 18446744073709551616.
-      simpl.
+      cbn.
       rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; omega).
       destruct (zlt i0_val 9223372036854775808) as [discard |]; try omega.
       clear discard.
@@ -449,7 +449,7 @@ Lemma big_unsigned_signed:
 Proof.
   destruct x as [xval xrange].
   intro BIG.
-  unfold Int.signed, Int.unsigned in *. simpl in *.
+  unfold Int.signed, Int.unsigned in *. cbn in *.
   destruct (zlt _ _).
   omega.
   trivial.
@@ -499,10 +499,10 @@ Lemma divs_is_quot: forall v1 v2 : val,
     end.
 
 Proof.
-  destruct v1; destruct v2; simpl; trivial.
+  destruct v1; destruct v2; cbn; trivial.
   unfold Int.divs.
   rewrite signed_0_eqb.
-  destruct (Int.eq i0 Int.zero) eqn:Eeq0; simpl; trivial.
+  destruct (Int.eq i0 Int.zero) eqn:Eeq0; cbn; trivial.
   destruct (Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:EXCEPTION.
   { replace (Int.signed i0) with (-1).
     replace (Int.signed i) with Int.min_signed.
@@ -523,7 +523,7 @@ Proof.
     unfold Int.eq in EXCEPTION.
     destruct (zeq _ _) in EXCEPTION; try discriminate.
     destruct (zeq _ _) as [Hmone | ]  in EXCEPTION; try discriminate.
-    destruct i0 as [i0val i0range]; unfold Int.signed in *; simpl in *.
+    destruct i0 as [i0val i0range]; unfold Int.signed in *; cbn in *.
     rewrite Hmone.
     reflexivity.
   }
@@ -651,7 +651,7 @@ Qed.
 Lemma sub_add_neg :
   forall x y, Val.sub x y = Val.add x (Val.neg y).
 Proof.
-  destruct x; destruct y; simpl; trivial.
+  destruct x; destruct y; cbn; trivial.
   f_equal.
   apply Int.sub_add_opp.
 Qed.
@@ -659,7 +659,7 @@ Qed.
 Lemma neg_mul_distr_r :
   forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y).
 Proof.
-  destruct x; destruct y; simpl; trivial.
+  destruct x; destruct y; cbn; trivial.
   f_equal.
   apply Int.neg_mul_distr_r.
 Qed.
@@ -668,7 +668,7 @@ Qed.
 Lemma sub_addl_negl :
   forall x y, Val.subl x y = Val.addl x (Val.negl y).
 Proof.
-  destruct x; destruct y; simpl; trivial.
+  destruct x; destruct y; cbn; trivial.
   + f_equal. apply Int64.sub_add_opp.
   + destruct (Archi.ptr64) eqn:ARCHI64; trivial.
     f_equal. rewrite Ptrofs.sub_add_opp.
@@ -681,15 +681,15 @@ Proof.
     rewrite Hagree2.
     reflexivity.
     exact (Ptrofs.agree64_of_int ARCHI64 i0).
-  +  destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial.
-     destruct (eq_block _ _); simpl; trivial.
+  +  destruct (Archi.ptr64) eqn:ARCHI64; cbn; trivial.
+     destruct (eq_block _ _); cbn; trivial.
 Qed.
  *)
 
 Lemma negl_mull_distr_r :
   forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y).
 Proof.
-  destruct x; destruct y; simpl; trivial.
+  destruct x; destruct y; cbn; trivial.
   f_equal.
   apply Int64.neg_mul_distr_r.
 Qed.