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 /powerpc/Op.v | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
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 'powerpc/Op.v')
| -rw-r--r-- | powerpc/Op.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v index e59e15f..58bcb2c 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -576,8 +576,8 @@ Proof. right. apply Int.no_overlap_sound; auto. (* Aglobal *) unfold symbol_address in *. - destruct (Genv.find_symbol ge i1) as []_eqn; inv H2. - destruct (Genv.find_symbol ge i) as []_eqn; inv H1. + destruct (Genv.find_symbol ge i1) eqn:?; inv H2. + destruct (Genv.find_symbol ge i) eqn:?; inv H1. destruct (ident_eq i i1). subst. replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)). replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)). @@ -587,9 +587,9 @@ Proof. left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto. (* Abased *) unfold symbol_address in *. - destruct (Genv.find_symbol ge i1) as []_eqn; simpl in *; try discriminate. + destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate. destruct v; inv H2. - destruct (Genv.find_symbol ge i) as []_eqn; inv H1. + destruct (Genv.find_symbol ge i) eqn:?; inv H1. destruct (ident_eq i i1). subst. rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3). right. apply Int.no_overlap_sound; auto. @@ -706,8 +706,8 @@ Opaque Int.add. Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b -> Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b). intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) as []_eqn; try discriminate. - destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) as []_eqn; try discriminate. + destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. rewrite (valid_pointer_inj _ H2 Heqb4). rewrite (valid_pointer_inj _ H Heqb0). simpl. destruct (zeq b1 b0); simpl in H1. @@ -792,7 +792,7 @@ Proof. inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2. exists (Vint i); auto. inv H4; inv H2; simpl; auto. - subst v1. destruct (eval_condition c vl1 m1) as []_eqn. + subst v1. destruct (eval_condition c vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. @@ -923,7 +923,7 @@ Hypothesis sp_inj: f sp1 = Some(sp2, delta). Remark symbol_address_inject: forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs). Proof. - intros. unfold symbol_address. destruct (Genv.find_symbol genv id) as []_eqn; auto. + intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. econstructor; eauto. rewrite Int.add_zero; auto. Qed. |