From 26d9fbb36b2e9c8f1262250035cd804bf87f7228 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 14 Jun 2021 19:02:39 +0200 Subject: Preparation for scheduling proof, main lemmas ok --- scheduling/BTL_Livecheck.v | 1 - 1 file changed, 1 deletion(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 25a1c545..9f96e74e 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -583,7 +583,6 @@ Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)) (LIVE: liveness_ok_function f) - (*(PC : (fn_code f) ! pc = Some ibf)*) (STACKS: list_forall2 eqlive_stackframes stk1 stk2), exists rs2' s', iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) -- cgit