diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 15:54:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-05 15:54:51 +0200 |
| commit | 9d94664fa180d909c43992a4cbdf6808fb9c4289 (patch) | |
| tree | dd6216f214debcbeeee32378d7b4b670e9de695d /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 7cf2665680872984dd62468b3e921276196d0290 (diff) | |
| download | compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.tar.gz compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.zip | |
#90 Asmvliw/Asmblock refactoring attempt
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index e0890a09..599a4024 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -21,7 +21,7 @@ Require Import Axioms. Local Open Scope error_monad_scope. -Definition match_prog (p tp: Asmblock.program) := +Definition match_prog (p tp: Asmvliw.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: @@ -826,7 +826,7 @@ Qed. Theorem transf_program_correct_Asmvliw: forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog). Proof. - eapply forward_simulation_step with (match_states:=fun (s1:Asmblock.state) s2 => s1=s2); eauto. + eapply forward_simulation_step with (match_states:=fun (s1:Asmvliw.state) s2 => s1=s2); eauto. - intros; subst; auto. - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto. + eapply exec_step_internal; eauto. |