diff options
Diffstat (limited to 'scheduling/BTL_Scheduler.v')
| -rw-r--r-- | scheduling/BTL_Scheduler.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index a3053add..39672749 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 := |