diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-14 11:42:11 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-14 11:42:11 +0100 |
| commit | afa25aac9373e4a7b37433ed861257a630264c29 (patch) | |
| tree | c835f6b8371d998f04e66347a7e6f9bb3eda3db4 /mppa_k1c/PostpassSchedulingproof.v | |
| parent | 802badd4bdf9b0e836935b74a25facb245558004 (diff) | |
| download | compcert-kvx-afa25aac9373e4a7b37433ed861257a630264c29.tar.gz compcert-kvx-afa25aac9373e4a7b37433ed861257a630264c29.zip | |
definition of VLIW semantics
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2de49faa..2e463f18 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -67,11 +67,10 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -Lemma next_eq {A: Type}: - forall (rs rs':A) m m', +Lemma next_eq rs rs' m m': rs = rs' -> m = m' -> Next rs m = Next rs' m'. Proof. - intros. congruence. + intros; apply f_equal2; auto. Qed. Lemma regset_double_set: @@ -659,8 +658,8 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. Qed. -Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). (* FIXME a remplacer par Asmvliw.semantics tprog *) Proof. eapply forward_simulation_plus. - apply senv_preserved. |