1 files changed, 0 insertions, 103 deletions
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
deleted file mode 100644
index dfc36b6..0000000
--- a/backend/Tunnelingtyping.v
+++ /dev/null
@@ -1,103 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Type preservation for the Tunneling pass *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import LTL.
-Require Import LTLtyping.
-Require Import Tunneling.
-Require Import Tunnelingproof.
-
-(** Tunneling preserves typing. *)
-
-Lemma branch_target_valid_1:
-  forall f pc, wt_function f ->
-  valid_successor f pc ->
-  valid_successor f (branch_target f pc).
-Proof.
-  intros. 
-  assert (forall n p,
-          (count_gotos f p < n)%nat ->
-          valid_successor f p ->
-          valid_successor f (branch_target f p)).
-  induction n; intros.
-  omegaContradiction.
-  elim H2; intros i EQ.
-  generalize (record_gotos_correct f p). rewrite EQ.
-  destruct i; try congruence.
-  intros [A | [B C]]. congruence. 
-  generalize (wt_instrs _ H _ _ EQ); intro WTI; inv WTI.
-  rewrite B. apply IHn. omega. auto. 
-
-  apply H1 with (Datatypes.S (count_gotos f pc)); auto.
-Qed.
-
-Lemma tunnel_valid_successor:
-  forall f pc,
-  valid_successor f pc -> valid_successor (tunnel_function f) pc.
-Proof.
-  intros. destruct H as [i AT].
-  unfold valid_successor; simpl. rewrite PTree.gmap. rewrite AT. 
-  simpl. exists (tunnel_instr (record_gotos f) i); auto.
-Qed.
-
-Lemma branch_target_valid:
-  forall f pc,
-  wt_function f ->
-  valid_successor f pc ->
-  valid_successor (tunnel_function f) (branch_target f pc).
-Proof.
-  intros. apply tunnel_valid_successor. apply branch_target_valid_1; auto.
-Qed.
-  
-Lemma wt_tunnel_instr:
-  forall f i,
-  wt_function f ->
-  wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i).
-Proof.
-  intros; inv H0; simpl; econstructor; eauto;
-  try (eapply branch_target_valid; eauto).
-  intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst lbl.
-  eapply branch_target_valid; eauto.
-  rewrite list_length_z_map. auto.
-Qed.
-
-Lemma wt_tunnel_function:
-  forall f, wt_function f -> wt_function (tunnel_function f).
-Proof.
-  intros. inversion H. constructor; simpl; auto.
-  intros until instr. rewrite PTree.gmap. unfold option_map. 
-  caseEq (fn_code f)!pc. intros b0 AT EQ. inv EQ. 
-  apply wt_tunnel_instr; eauto.
-  congruence.
-  eapply branch_target_valid; eauto.
-Qed.
-
-Lemma wt_tunnel_fundef:
-  forall f, wt_fundef f -> wt_fundef (tunnel_fundef f).
-Proof.
-  intros. inversion H; simpl. constructor; auto. 
-  constructor. apply wt_tunnel_function; auto.
-Qed.
-
-Lemma program_typing_preserved:
-  forall (p: LTL.program),
-  wt_program p -> wt_program (tunnel_program p).
-Proof.
-  intros; red; intros.
-  generalize (transform_program_function tunnel_fundef p i f H0).
-  intros [f0 [IN TRANSF]].
-  subst f. apply wt_tunnel_fundef. eauto.
-Qed.