diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-17 23:19:16 +0200 |
| commit | bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 (patch) | |
| tree | 87696f4b78894ceb46d44b1d7e2aea9375865c5d /scheduling/RTLtoBTL.v | |
| parent | ee558407e59c6794daad70aab2e1e7794535367e (diff) | |
| download | compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.tar.gz compcert-kvx-bf443e2f2bf38c30c9b68020c7c43cd7b3e10549.zip | |
preparing compiler passes and ml oracles
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. |