aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicateaux.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 /backend/Duplicateaux.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 'backend/Duplicateaux.ml')
-rw-r--r--backend/Duplicateaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index e8e60a4f..8ca6c6ab 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -23,7 +23,7 @@ open RTL
open Maps
open Camlcoq
open DebugPrint
-open AuxTools
+open RTLcommonaux
let stats_oc = ref None