1 files changed, 2 insertions, 19 deletions
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 72a4ee01..a9c2fa76 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -260,19 +260,6 @@ Proof.
     + rewrite <- H. erewrite <- seval_preserved; eauto.
 Qed.
 
-Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
-  ipath_checker path f (fn_path f) alive pc = Some res
-  -> nth_default_succ (fn_code f) path pc = Some (snd res).
-Proof.
-  induction path; simpl.
-  + try_simplify_someHyps.
-  + intros alive pc res.
-    inversion_SOME i; intros INST.
-    inversion_SOME res0; intros ICHK IPCHK.
-    rewrite INST.
-    erewrite iinst_checker_default_succ; eauto.
-Qed.
-
 Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
   (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
           (irs is) (imem is) t s)
@@ -331,17 +318,14 @@ Qed.
 Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
   (liveness_ok_function f) ->
   (fn_path f) ! pc0 = Some path0 ->
-  (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *)  (* NB: should be useless *)
   sexec f pc0 = Some st -> 
-  (* icontinue is = true -> *)
   list_forall2 match_stackframes stk stk' ->
-  (* ssem_internal ge sp st rs0 m0 is -> *)
   ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
   eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
   exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
 Proof.
   Local Hint Resolve eqlive_stacks_refl: core.
-  intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
+  intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE.
   (* start decomposing path_checker *)
   generalize (LIVE pc0 path0 PATH0).
   unfold path_checker.
@@ -413,7 +397,6 @@ Qed.
 (* The main theorem on simulation of symbolic states ! *)
 Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
   (fn_path f) ! pc0 = Some path0 ->
-  (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *)
   sexec f pc0 = Some st -> 
   match_function dm f f' ->
   liveness_ok_function f ->
@@ -422,7 +405,7 @@ Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
   (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
   exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
 Proof.
-  intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
+  intros PATH0 SEXEC MFUNC LIVE STACKS SEM SIMU.
   destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
   destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
   - (* sem_early *)