From 9976ed7a27434cfcc334959ef5f20e4967ff8dcb Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 28 Mar 2010 10:01:53 +0000 Subject: Updating ARM port git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Op.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v index 51ce0024..7a255115 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -572,8 +572,7 @@ Proof. destruct v; destruct chunk; exact I. intros until v. unfold Mem.loadv. destruct addr; intros; try discriminate. - generalize (Mem.load_inv _ _ _ _ _ H0). - intros [X Y]. subst v. apply H. + eapply Mem.load_type; eauto. Qed. End SOUNDNESS. -- cgit