diff options
Diffstat (limited to 'backend/RTLTunneling.v')
| -rw-r--r-- | backend/RTLTunneling.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index e6901a9f..049160fd 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -25,6 +25,7 @@ Definition UF := PTree.t (node * Z). (* The oracle returns a map of "nop" node to their target with a distance (ie the number of the "nop" node on the path) to the target. *) Axiom branch_target: RTL.function -> UF. +Extract Constant branch_target => "RTLTunnelingaux.branch_target". (* TODO: add an extraction command to link branch_target with its implementation *) Local Open Scope error_monad_scope. |