diff options
Diffstat (limited to 'scheduling/BTLtoRTL.v')
| -rw-r--r-- | scheduling/BTLtoRTL.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v index b64fd87a..82ad47b1 100644 --- a/scheduling/BTLtoRTL.v +++ b/scheduling/BTLtoRTL.v @@ -5,7 +5,9 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking. (** External oracle *) -Parameter btl2rtl: function -> RTL.code * node * (PTree.t node). +Axiom btl2rtl: function -> RTL.code * node * (PTree.t node). + +Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl". Local Open Scope error_monad_scope. |