From ab520acd80f7d39aa14fdda6932accbb2a787ebf Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 12:47:22 +0200 Subject: Grouping common RTL functions, printer improvement --- backend/Duplicateaux.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Duplicateaux.ml') 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 *) -- cgit