diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 17:16:55 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 17:16:55 +0000 |
| commit | 5a4bd6f2636df432383bb3144f91816742d2fa53 (patch) | |
| tree | 9f08067aebd72e17dd0d3ae79f99c7e279284ee7 /powerpc/Asmgenproof1.v | |
| parent | abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 (diff) | |
| download | compcert-kvx-5a4bd6f2636df432383bb3144f91816742d2fa53.tar.gz compcert-kvx-5a4bd6f2636df432383bb3144f91816742d2fa53.zip | |
Renamed Machconcr into Machsem.
Removed Machabstr and Machabstr2concr, now useless following the reengineering
of Stacking.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 16dd923e..a0cdeabc 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -23,7 +23,7 @@ Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. -Require Import Machconcr. +Require Import Machsem. Require Import Machtyping. Require Import Asm. Require Import Asmgen. @@ -486,7 +486,7 @@ Lemma extcall_arg_match: forall ms sp rs m m' l v, agree ms sp rs -> Mem.extends m m' -> - Machconcr.extcall_arg ms m sp l v -> + Machsem.extcall_arg ms m sp l v -> exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. Proof. intros. inv H1. @@ -503,7 +503,7 @@ Qed. Lemma extcall_args_match: forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall ll vl, - Machconcr.extcall_args ms m sp ll vl -> + Machsem.extcall_args ms m sp ll vl -> exists vl', Asm.extcall_args rs m' ll vl' /\ Val.lessdef_list vl vl'. Proof. induction 3; intros. @@ -516,10 +516,10 @@ Qed. Lemma extcall_arguments_match: forall ms m m' sp rs sg args, agree ms sp rs -> Mem.extends m m' -> - Machconcr.extcall_arguments ms m sp sg args -> + Machsem.extcall_arguments ms m sp sg args -> exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. Proof. - unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros. + unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros. eapply extcall_args_match; eauto. Qed. |