From 9d94664fa180d909c43992a4cbdf6808fb9c4289 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 5 Apr 2019 15:54:51 +0200 Subject: #90 Asmvliw/Asmblock refactoring attempt --- mppa_k1c/lib/Asmblockgenproof0.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/lib') 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). -- cgit