From fa0c79015c3ecd2ad63dbf1b50f60039cf043151 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 17 Nov 2020 16:11:43 +0100
Subject: Builtin mem spec in scheduler and some needed proof in Postpasssch.v

---
 aarch64/PostpassScheduling.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'aarch64/PostpassScheduling.v')

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) 
-- 
cgit