aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.vexpand
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Compiler.vexpand')
-rw-r--r--driver/Compiler.vexpand2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index 40ea0d68..1d218657 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -300,6 +300,8 @@ EXPAND_RTL_FORWARD_SIMULATIONS
eapply compose_forward_simulations.
eapply RTLtoBTLproof.transf_program_correct; eassumption.
eapply compose_forward_simulations.
+ eapply BTL_Schedulerproof.transf_program_correct; eassumption.
+ eapply compose_forward_simulations.
eapply BTLtoRTLproof.transf_program_correct; eassumption.
eapply compose_forward_simulations.
eapply Allocationproof.transf_program_correct; eassumption.