diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 513ed40a..f5c2f3db 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -743,7 +743,7 @@ Theorem transf_program_correct: Proof. eapply compose_forward_simulations. - eapply transf_program_correct_cfg. - - eapply cfgsem2fsem. + - eapply cfgsem2fsem. eauto. Admitted. End BTL_SIMULATES_RTL. |