diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-12 12:55:21 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-12 12:55:21 +0000 |
| commit | aaa49526068f528f2233de0dace43549432fba52 (patch) | |
| tree | e675fe11f225858ddd290594fa5ffed2865d5677 /backend/Reloadtyping.v | |
| parent | 845148dea58bbdd041c399a8c9196d9e67bec629 (diff) | |
| download | compcert-aaa49526068f528f2233de0dace43549432fba52.tar.gz compcert-aaa49526068f528f2233de0dace43549432fba52.zip | |
Revu gestion retaddr et link dans Stacking
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Reloadtyping.v')
| -rw-r--r-- | backend/Reloadtyping.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 3f0ff1ee..2edb4827 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -300,12 +300,13 @@ Proof. inv H. inv H1. constructor. unfold wt_function. simpl. apply wt_parallel_move; auto with reloadty. rewrite loc_parameters_type. auto. - unfold loc_parameters; red; intros. - destruct (list_in_map_inv _ _ _ H) as [r [A B]]. rewrite A. - generalize (loc_arguments_acceptable _ _ B). - destruct r; simpl; auto. destruct s; try tauto. - intros; simpl. split. omega. - apply loc_arguments_bounded; auto. + red; intros. + destruct (list_in_map_inv _ _ _ H) as [r [A B]]. + generalize (loc_arguments_acceptable _ _ B). + destruct r; intro. + rewrite A. simpl. auto. + red in H0. destruct s; try tauto. + simpl in A. subst l. simpl. auto. apply wt_transf_code; auto. constructor. Qed. |