diff options
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 5232f903..1483a5d7 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -19,6 +19,8 @@ Local Open Scope error_monad_scope. returns a schedule expressed as a list of bundles *) Axiom schedule: bblock -> list bblock. +Extract Constant schedule => "PostpassSchedulingOracle.schedule". + (* TODO - implement the verificator *) Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb). |