diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |