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/Op.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'ia32/Op.v') diff --git a/ia32/Op.v b/ia32/Op.v index 8169594..93a867a 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -642,8 +642,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)). @@ -653,9 +653,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. @@ -776,8 +776,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. @@ -878,7 +878,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; simpl in H1; inv H1. simpl. TrivialExists. - 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. @@ -995,7 +995,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. -- cgit v1.2.3