diff options
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 8ad30e81..2de49faa 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -575,9 +575,9 @@ Lemma transf_exec_basic_instr: Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. exploreInst; simpl; auto; try congruence. - 1: unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. - 1-10: apply transf_exec_load. - all: apply transf_exec_store. + - unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. + - apply transf_exec_load. + - apply transf_exec_store. Qed. Lemma transf_exec_body: |