aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml8
1 files changed, 0 insertions, 8 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml
index 7fc940c7..4e89b28c 100644
--- a/scheduling/MyRTLpathScheduleraux.ml
+++ b/scheduling/MyRTLpathScheduleraux.ml
@@ -1062,14 +1062,6 @@ let my_merge_no_overwrite m1 m2 =
else failwith "Merge conflict."
) m1 m2
-let my_merge_overwrite m1 m2 =
- PTree.combine (fun x y -> match (x, y) with
- | None, None -> None
- | Some x, None
- | None, Some x -> Some x
- | Some _, Some y -> Some y
- ) m1 m2
-
let print_schedule schedule =
debug "Schedule\n";
Array.iter (fun pos -> debug "%d\n" (Camlcoq.P.to_int pos)) schedule;