diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-07 08:06:23 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-07 08:06:23 +0200 |
| commit | 7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2 (patch) | |
| tree | 2951ff922c42f813e621181d13cb8f93102e7f2d /mppa_k1c/lib | |
| parent | 7946ed0e9130e164c39e137115419ea0ed158c9f (diff) | |
| download | compcert-kvx-7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2.tar.gz compcert-kvx-7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2.zip | |
extract Machgen.trans_code stuff from Asmgenproof
Diffstat (limited to 'mppa_k1c/lib')
| -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 -> |