diff options
Diffstat (limited to 'mppa_k1c/lib/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 443e8757..86c81c8d 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -14,6 +14,7 @@ Require Import Machblock. Require Import Asmblock. Require Import Asmblockgen. Require Import Conventions1. +Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) Module MB:=Machblock. Module AB:=Asmblock. @@ -571,21 +572,6 @@ Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : P transl_blocks f c false = OK tc -> code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc. -(* NB: these two lemma should go into [Coqlib.v] *) -Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). -Proof. - induction l1; simpl; auto with coqlib. -Qed. -Hint Resolve is_tail_app: coqlib. - -Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. -Proof. - induction l1; simpl; auto with coqlib. - intros l2 l3 H; inversion H; eauto with coqlib. -Qed. -Hint Resolve is_tail_app_inv: coqlib. - - Lemma transl_blocks_tail: forall f c1 c2, is_tail c1 c2 -> forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 -> |