diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
| commit | 056068abd228fefab4951a61700aa6d54fb88287 (patch) | |
| tree | 6bf44526caf535e464e33999641b39032901fa67 /arm/ConstpropOpproof.v | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
| download | compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.tar.gz compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.zip | |
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/ConstpropOpproof.v')
| -rw-r--r-- | arm/ConstpropOpproof.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 4c38d5ea..e7e6a419 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -149,7 +149,7 @@ Proof. destruct (propagate_float_constants tt); simpl; auto. destruct (propagate_float_constants tt); simpl; auto. unfold eval_static_condition_val, Val.of_optbool. - destruct (eval_static_condition c vl0) as []_eqn. + destruct (eval_static_condition c vl0) eqn:?. rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). destruct b; simpl; auto. simpl; auto. @@ -247,7 +247,7 @@ Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shl_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -261,7 +261,7 @@ Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shr_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -275,7 +275,7 @@ Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.shru_zero. auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; intros. + destruct (Int.ltu n Int.iwordsize) eqn:?; intros. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. econstructor; split; eauto. simpl. congruence. Qed. @@ -291,7 +291,7 @@ Proof. exists (Vint Int.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_zero; auto. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int.mul_one; auto. - destruct (Int.is_power2 n) as []_eqn; intros. + destruct (Int.is_power2 n) eqn:?; intros. exploit Int.is_power2_range; eauto. intros R. econstructor; split. simpl; eauto. rewrite mk_shift_amount_eq; auto. rewrite (Val.mul_pow2 rs#r1 _ _ Heqo). auto. @@ -306,8 +306,8 @@ Lemma make_divimm_correct: exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. - destruct (Int.is_power2 n) as []_eqn. - destruct (Int.ltu i (Int.repr 31)) as []_eqn. + destruct (Int.is_power2 n) eqn:?. + destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. exists v; auto. exists v; auto. @@ -321,7 +321,7 @@ Lemma make_divuimm_correct: exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. - destruct (Int.is_power2 n) as []_eqn. + destruct (Int.is_power2 n) eqn:?. replace v with (Val.shru rs#r1 (Vint i)). econstructor; split. simpl. rewrite mk_shift_amount_eq. eauto. eapply Int.is_power2_range; eauto. auto. |