From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 31 May 2021 16:55:18 +0200 Subject: BTL Scheduler oracle and some drafts --- driver/Compiler.vexpand | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 85f265db..40ea0d68 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -300,7 +300,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLtoBTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply BTLtoRTLproof.transf_program_correct_cfg; eassumption. + eapply BTLtoRTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit