From bf443e2f2bf38c30c9b68020c7c43cd7b3e10549 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 23:19:16 +0200 Subject: preparing compiler passes and ml oracles --- scheduling/BTLtoRTL.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'scheduling/BTLtoRTL.v') 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. -- cgit