From 43ab0b948ac379e55bbe334a0a541c1680437fbf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 10:40:54 +0200 Subject: most of the proof BTL.fsem -> BTL.cfgsem. --- scheduling/RTLtoBTLproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 60edea49..feaac26f 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -727,9 +727,9 @@ Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (BTL.semantics tprog). + forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog). Proof. - eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=semantics tprog) (ltof _ omeasure) match_states). + eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). constructor 1; simpl. - apply well_founded_ltof. - eapply transf_initial_states. -- cgit