aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/Linearizeaux.ml2
-rw-r--r--backend/PrintLTL.ml2
-rw-r--r--backend/PrintRTL.ml2
-rw-r--r--backend/PrintXTL.ml2
4 files changed, 4 insertions, 4 deletions
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 46d5c3f1..902724e0 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -106,7 +106,7 @@ let flatten_blocks blks =
let cmp_minpc (mpc1, _) (mpc2, _) =
if mpc1 = mpc2 then 0 else if mpc1 > mpc2 then -1 else 1
in
- List.flatten (List.map Pervasives.snd (List.sort cmp_minpc blks))
+ List.flatten (List.map snd (List.sort cmp_minpc blks))
(* Build the enumeration *)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index d0557073..1c449e74 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -112,7 +112,7 @@ let print_function pp id f =
fprintf pp "%s() {\n" (extern_atom id);
let instrs =
List.sort
- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
(List.rev_map
(fun (pc, i) -> (P.to_int pc, i))
(PTree.elements f.fn_code)) in
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index ba336b0a..841540b6 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -93,7 +93,7 @@ let print_function pp id f =
fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
let instrs =
List.sort
- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
(List.rev_map
(fun (pc, i) -> (P.to_int pc, i))
(PTree.elements f.fn_code)) in
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index cc1f7d49..6432682a 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -138,7 +138,7 @@ let print_function pp ?alloc ?live f =
fprintf pp "f() {\n";
let instrs =
List.sort
- (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
+ (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
(List.map
(fun (pc, i) -> (P.to_int pc, i))
(PTree.elements f.fn_code)) in