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/lib | |
| parent | 7cf2665680872984dd62468b3e921276196d0290 (diff) | |
| download | compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.tar.gz compcert-kvx-9d94664fa180d909c43992a4cbdf6808fb9c4289.zip | |
#90 Asmvliw/Asmblock refactoring attempt
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index d0e05389..8a83521c 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -16,7 +16,7 @@ Require Import Asmblockgen. Require Import Conventions1. Module MB:=Machblock. -Module AB:=Asmblock. +Module AB:=Asmvliw. Hint Extern 2 (_ <> _) => congruence: asmgen. @@ -311,9 +311,9 @@ Qed. Lemma agree_undef_caller_save_regs: forall ms sp rs, agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (Asmblock.undef_caller_save_regs rs). + agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs). Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, Asmblock.undef_caller_save_regs; split. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split. - unfold proj_sumbool; rewrite dec_eq_true. auto. - auto. - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). |