aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Duplicateaux.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-19 12:47:22 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-05-19 12:47:22 +0200
commitab520acd80f7d39aa14fdda6932accbb2a787ebf (patch)
tree67adb8d133f32cd4a64e0d21270632f60866355a /backend/Duplicateaux.ml
parentaf2208a2c7126d4d101fb07c40920e12c9ebbab3 (diff)
downloadcompcert-kvx-ab520acd80f7d39aa14fdda6932accbb2a787ebf.tar.gz
compcert-kvx-ab520acd80f7d39aa14fdda6932accbb2a787ebf.zip
Grouping common RTL functions, printer improvement
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 d55da64a..e8e60a4f 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -23,6 +23,7 @@ open RTL
open Maps
open Camlcoq
open DebugPrint
+open AuxTools
let stats_oc = ref None
@@ -95,7 +96,6 @@ let write_stats_oc () =
end
let get_loop_headers = LICMaux.get_loop_headers
-let get_some = LICMaux.get_some
let rtl_successors = LICMaux.rtl_successors
(* Get list of nodes following a BFS of the code *)