1 files changed, 0 insertions, 50 deletions
diff --git a/scheduling/RTLpathproof.v b/scheduling/RTLpathproof.v
deleted file mode 100644
index 20eded97..00000000
--- a/scheduling/RTLpathproof.v
+++ /dev/null
@@ -1,50 +0,0 @@
-Require Import Coqlib Maps.
-Require Import AST Integers Values Events Memory Globalenvs Smallstep.
-Require Import Op Registers.
-Require Import RTL Linking.
-Require Import RTLpath.
-
-Definition match_prog (p: RTLpath.program) (tp: RTL.program) :=
-  match_program (fun ctx f tf => tf = fundef_RTL f) eq p tp.
-
-Lemma transf_program_match:
-  forall p, match_prog p (transf_program p).
-Proof.
-  intros. eapply match_transform_program; eauto.
-Qed.
-
-Lemma match_program_transf:
-  forall p tp, match_prog p tp -> transf_program p = tp.
-Proof.
-  intros p tp H. inversion_clear H. inv H1.
-  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
-  subst. unfold transf_program. unfold transform_program. simpl.
-  apply program_equals; simpl; auto.
-  induction H0; simpl; auto.
-  rewrite IHlist_forall2. apply cons_extract.
-  destruct a1 as [ida gda]. destruct b1 as [idb gdb].
-  simpl in *.
-  inv H. inv H2.
-  - simpl in *. subst. auto.
-  - simpl in *. subst. inv H. auto.
-Qed.
-
-
-Section PRESERVATION.
-
-Variable prog: RTLpath.program.
-Variable tprog: RTL.program.
-Hypothesis TRANSF: match_prog prog tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-Theorem transf_program_correct:
-  forward_simulation (RTLpath.semantics prog) (RTL.semantics tprog).
-Proof.
-  pose proof (match_program_transf prog tprog TRANSF) as TR. subst.
-  eapply RTLpath_correct.
-Qed.
-
-End PRESERVATION.
-
-