aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-07-29 13:04:58 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-07-29 13:04:58 +0200
commit5628b922283c40b8169b68d13c5bdc43accf2366 (patch)
treeb7b06014a56b5a3e42d4b8e948c9ef6798efbf54
parent6b9bb0e4ba2c4ad842a6de3073978209349559bb (diff)
downloadcompcert-kvx-5628b922283c40b8169b68d13c5bdc43accf2366.tar.gz
compcert-kvx-5628b922283c40b8169b68d13c5bdc43accf2366.zip
Add convenience, map-like, function to InsertPosition
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml
index beb6cbf8..93c3da21 100644
--- a/scheduling/MyRTLpathScheduleraux.ml
+++ b/scheduling/MyRTLpathScheduleraux.ml
@@ -134,6 +134,10 @@ module InsertPosition = struct
| Below of Camlcoq.P.t
let anchor = function
| Above x | Below x -> x
+
+ let pseudo_map pos ~f = match pos with
+ | Above x -> Above (f x)
+ | Below x -> Below (f x)
let compare x y =
match Camlcoq.P.compare (anchor x) (anchor y) with
| 0 -> (match x, y with