From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: 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 --- ia32/SelectOpproof.v | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'ia32/SelectOpproof.v') diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 136a765..18deca6 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -228,12 +228,12 @@ Proof. destruct (shlimm_match a); intros; InvEval. exists (Vint (Int.shl n1 n)); split. EvalOp. simpl. destruct (Int.ltu n Int.iwordsize); auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp. subst. destruct v1; simpl; auto. rewrite Heqb. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto. rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. @@ -259,12 +259,12 @@ Proof. destruct (shruimm_match a); intros; InvEval. exists (Vint (Int.shru n1 n)); split. EvalOp. simpl. destruct (Int.ltu n Int.iwordsize); auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp. subst. destruct v1; simpl; auto. rewrite Heqb. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. @@ -281,12 +281,12 @@ Proof. destruct (shrimm_match a); intros; InvEval. exists (Vint (Int.shr n1 n)); split. EvalOp. simpl. destruct (Int.ltu n Int.iwordsize); auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp. subst. destruct v1; simpl; auto. rewrite Heqb. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto. - destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. + destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto. rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. @@ -417,25 +417,25 @@ Proof. InvEval. rewrite Val.or_commut. apply eval_orimm; auto. InvEval. apply eval_orimm; auto. (* shlimm - shruimm *) - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. exists (Val.ror v0 (Vint n2)); split. EvalOp. destruct v0; simpl; auto. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. - destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. + destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. simpl. rewrite <- Int.or_ror; auto. TrivialExists. (* shruimm - shlimm *) - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?. destruct (andb_prop _ _ Heqb0). generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. exists (Val.ror v1 (Vint n2)); split. EvalOp. destruct v1; simpl; auto. - destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. - destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. + destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. TrivialExists. (* default *) @@ -717,7 +717,7 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros. destruct x; simpl in H0; try discriminate. - destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0. + destruct (Float.intuoffloat f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. set (im := Int.repr Int.half_modulus). set (fm := Float.floatofintu im). @@ -729,7 +729,7 @@ Proof. econstructor. instantiate (1 := Vfloat fm). EvalOp. eapply eval_Econdition with (vb := Float.cmp Clt f fm). eauto with evalexpr. auto. - destruct (Float.cmp Clt f fm) as []_eqn. + destruct (Float.cmp Clt f fm) eqn:?. exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. exploit Float.intuoffloat_intoffloat_2; eauto. @@ -763,7 +763,7 @@ Proof. eapply eval_Econdition with (vb := Int.ltu i Float.ox8000_0000). constructor. eauto. constructor. simpl. auto. - destruct (Int.ltu i Float.ox8000_0000) as []_eqn. + destruct (Int.ltu i Float.ox8000_0000) eqn:?. rewrite Float.floatofintu_floatofint_1; auto. unfold floatofint. EvalOp. exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto. -- cgit v1.2.3