Updating ARM port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1 insertions, 2 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 51ce002..7a25511 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.