From e9704f237a400630ba45ee65779123b054dc1d6c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 17 May 2013 08:59:15 +0000 Subject: Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2254 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Asmgenproof.v') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index aede0da4..68990409 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -693,7 +693,7 @@ Opaque loadind. exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. unfold Mach.chunk_of_type in A. rewrite A. + simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. @@ -896,7 +896,7 @@ Opaque loadind. rewrite <- H5 at 2; unfold fn_code. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold Mach.chunk_of_type in F. rewrite F. auto. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. -- cgit