remove todos, clean

1 files changed, 0 insertions, 47 deletions

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 40ad0d88..9a73d278 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -45,53 +45,6 @@ Proof.
   + eapply linkorder_refl.
 Qed.
 
-(* TODO gourdinl move this to BTL_Scheduler.v? *)
-Inductive match_fundef: fundef -> fundef -> Prop :=
-  | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
-  | match_External ef: match_fundef (External ef) (External ef).
-
-Inductive match_stackframes: stackframe -> stackframe -> Prop :=
-  | match_stackframe_intro 
-      res f sp pc rs rs' f'
-      (EQREGS: forall r, rs # r = rs' # r)
-      (TRANSF: match_function f f')
-      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs').
-
-Inductive match_states: state -> state -> Prop :=
-  | match_states_intro 
-      st f sp pc rs rs' m st' f'
-      (EQREGS: forall r, rs # r = rs' # r)
-      (STACKS: list_forall2 match_stackframes st st')
-      (TRANSF: match_function f f')
-      : match_states (State st f sp pc rs m) (State st' f' sp pc rs' m)
-  | match_states_call
-      st st' f f' args m
-      (STACKS: list_forall2 match_stackframes st st')
-      (TRANSF: match_fundef f f')
-      : match_states (Callstate st f args m) (Callstate st' f' args m)
-  | match_states_return
-      st st' v m
-      (STACKS: list_forall2 match_stackframes st st')
-      : match_states (Returnstate st v m) (Returnstate st' v m)
-   .
-
-Lemma match_stack_equiv stk1 stk2:
-  list_forall2 match_stackframes stk1 stk2 -> 
-  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
-  list_forall2 match_stackframes stk1 stk3.
-Proof.
-  induction 1; intros stk3 EQ; inv EQ; constructor; eauto.
-  inv H3; inv H; econstructor; eauto.
-  intros; rewrite <- EQUIV; auto.
-Qed.
-
-Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
-Proof.
-  Local Hint Resolve match_stack_equiv: core.
-  destruct 1; intros EQ; inv EQ; econstructor; eauto.
-  intros; rewrite <- EQUIV; auto.
-Qed.
-
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> match_function f f'.
 Proof.