From 9ce1b23f6361d8070490df1269a7bc53aa215efb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 12:16:27 +0200 Subject: expansions btl proofs --- scheduling/BTL_Scheduler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL_Scheduler.v') diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 39672749..a3053add 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -113,7 +113,7 @@ Qed. Definition transf_function (f: BTL.function) := let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in - (*do _ <- check_symbolic_simu f tf;*) + do _ <- check_symbolic_simu f tf; OK tf. Definition transf_fundef (f: fundef) : res fundef := -- cgit