diff options
Diffstat (limited to 'aarch64/PostpassScheduling.v')
| -rw-r--r-- | aarch64/PostpassScheduling.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index c84b327b..a9473789 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -336,8 +336,9 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re | Some c => OK {| header := nil; body := lb; exit := Some c |} end. Next Obligation. - (* TODO *) -Admitted. + unfold Is_true, AB.non_empty_bblockb. + unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity. +Qed. Definition do_schedule (bb: bblock) : res bblock := if (Z.eqb (size bb) 1) then OK (bb) |