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