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 --- backend/RREproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/RREproof.v') diff --git a/backend/RREproof.v b/backend/RREproof.v index 8926fe4f..40632f74 100644 --- a/backend/RREproof.v +++ b/backend/RREproof.v @@ -248,7 +248,7 @@ Proof. induction ll; intros; simpl. apply H. simpl. auto. apply IHll. intros. unfold Locmap.set. - destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) as []_eqn. auto. + destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) eqn:?. auto. apply H. simpl. split; auto. apply Loc.diff_sym. apply Loc.non_overlap_diff; auto. Qed. @@ -396,7 +396,7 @@ Opaque destroyed_at_move_regs. simpl in SAFE. assert (SAFE': sm = false \/ ~In r destroyed_at_move_regs /\ safe_move_insertion b = true). destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. - destruct (is_incoming sl) as []_eqn. + destruct (is_incoming sl) eqn:?. (* incoming, stays as getstack *) assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs). destruct sl; simpl in Heqb0; discriminate || auto. @@ -419,11 +419,11 @@ Opaque destroyed_at_move_regs. rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same. apply match_states_regular with sm; auto; tauto. (* found an equation *) - destruct (find_reg_containing sl eqs) as [r'|]_eqn. + destruct (find_reg_containing sl eqs) as [r'|] eqn:?. exploit EQH. eapply find_reg_containing_sound; eauto. simpl; intro EQ. (* turned into a move *) - destruct (safe_move_insertion b) as []_eqn. + destruct (safe_move_insertion b) eqn:?. left; econstructor; split. constructor. simpl; eauto. rewrite UGS. rewrite <- EQ. apply match_states_regular with true; auto. -- cgit