simpl -> cbn

1 files changed, 17 insertions, 17 deletions

diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v
index ab30ded9..0b2cf406 100644
--- a/kvx/Conventions1.v
+++ b/kvx/Conventions1.v
@@ -108,7 +108,7 @@ Lemma loc_result_type:
   subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
 Proof.
   intros. unfold proj_sig_res, loc_result, mreg_type.
-  destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial.
+  destruct (sig_res sig); try destruct Archi.ptr64; cbn; trivial; destruct t; trivial.
 Qed.
 
 (** The result locations are caller-save registers *)
@@ -118,7 +118,7 @@ Lemma loc_result_caller_save:
   forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
   intros. unfold loc_result, is_callee_save;
-            destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto.
+            destruct (sig_res s); cbn; auto; try destruct Archi.ptr64; cbn; auto; try destruct t; cbn; auto.
 Qed.
 
 (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -296,9 +296,9 @@ Proof.
              OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
   { intros until f; intros OR OF OO; red; unfold one_arg; intros.
     destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
+  - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
-  - subst p; simpl. auto using align_divides, typealign_pos.
+  - subst p; cbn. auto using align_divides, typealign_pos.
   - eapply OF; [idtac|eauto].
     generalize (AL ofs ty OO) (SKK ty); omega.
   }
@@ -310,16 +310,16 @@ Proof.
     assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto).
     assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint)
                      :: f rn' (ofs' + 2))).
-    { red; simpl; intros. destruct H.
-    - subst p; simpl. 
+    { red; cbn; intros. destruct H.
+    - subst p; cbn. 
       repeat split; auto using Z.divide_1_l. omega.
     - eapply OF; [idtac|eauto]. omega.
     }
     destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
     destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
     try apply DFL.
-    red; simpl; intros; destruct H.
-  - subst p; simpl. split; apply OR; eauto using list_nth_z_in.  
+    red; cbn; intros; destruct H.
+  - subst p; cbn. split; apply OR; eauto using list_nth_z_in.  
   - eapply OF; [idtac|eauto]. auto.
   }
   assert (C: forall regs rn ofs ty f,
@@ -327,10 +327,10 @@ Proof.
   { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros.
     set (rn' := align rn 2) in *.
     destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
+  - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
-  - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
-  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega.
+  - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
+  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega.
   }
   assert (D: OKREGS param_regs).
   { red. decide_goal. }
@@ -339,8 +339,8 @@ Proof.
 
   cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)).
   unfold OK. eauto.
-  induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
-  - red; simpl; tauto.
+  induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; cbn.
+  - red; cbn; tauto.
   - destruct ty1.  
 + (* int *) apply A; auto.
 + (* float *) 
@@ -369,10 +369,10 @@ Remark fold_max_outgoing_above:
 Proof.
   assert (A: forall n l, max_outgoing_1 n l >= n).
   { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
-  induction l; simpl; intros. 
+  induction l; cbn; intros. 
   - omega.
   - eapply Zge_trans. eauto.
-    destruct a; simpl. apply A. eapply Zge_trans; eauto.
+    destruct a; cbn. apply A. eapply Zge_trans; eauto.
 Qed.
 
 Lemma size_arguments_above:
@@ -392,14 +392,14 @@ Proof.
   assert (B: forall p n,
              In (S Outgoing ofs ty) (regs_of_rpair p) ->
              ofs + typesize ty <= max_outgoing_2 n p).
-  { intros. destruct p; simpl in H; intuition; subst; simpl.
+  { intros. destruct p; cbn in H; intuition; subst; cbn.
   - xomega.
   - eapply Z.le_trans. 2: apply A. xomega.
   - xomega. }
   assert (C: forall l n,
              In (S Outgoing ofs ty) (regs_of_rpairs l) ->
              ofs + typesize ty <= fold_left max_outgoing_2 l n).
-  { induction l; simpl; intros.
+  { induction l; cbn; intros.
   - contradiction.
   - rewrite in_app_iff in H. destruct H.
   + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above.