aboutsummaryrefslogtreecommitdiffstats
path: root/common
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 /common
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 'common')
-rw-r--r--common/DebugPrint.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml
index 021ea5c0..d94b31d8 100644
--- a/common/DebugPrint.ml
+++ b/common/DebugPrint.ml
@@ -1,7 +1,7 @@
open Maps
open Camlcoq
open Registers
-open AuxTools
+open RTLcommonaux
let debug_flag = ref false