aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTLtoRTLaux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-24 10:07:52 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-24 10:07:52 +0200
commit0efe7783c50d72858352fda93d30e0f52792d658 (patch)
treecba55c0122b0260000d85278c6b1a46b6d30b202 /scheduling/BTLtoRTLaux.ml
parent30e41117b57ab20beb1876e38c26dbddc5a58dfb (diff)
downloadcompcert-kvx-0efe7783c50d72858352fda93d30e0f52792d658.tar.gz
compcert-kvx-0efe7783c50d72858352fda93d30e0f52792d658.zip
Moving common tools, adding liveness input/output information to BTL generation oracle
Diffstat (limited to 'scheduling/BTLtoRTLaux.ml')
-rw-r--r--scheduling/BTLtoRTLaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index 36d3e6a4..521f6ef2 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -2,7 +2,7 @@ open Maps
open BTL
open RTL
open Camlcoq
-open AuxTools
+open RTLcommonaux
open DebugPrint
open BTLaux