aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Coloring.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Coloring.v')
-rw-r--r--backend/Coloring.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 0a2487cb..0b8a4ccc 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -81,8 +81,8 @@ Require Import InterfGraph.
Definition add_interf_live
(filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
- Regset.fold
- (fun g r => if filter r then add_interf r res g else g) live g.
+ Regset.fold graph
+ (fun r g => if filter r then add_interf r res g else g) live g.
Definition add_interf_op
(res: reg) (live: Regset.t) (g: graph): graph :=
@@ -101,7 +101,7 @@ Definition add_interf_move
Definition add_interf_call
(live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
List.fold_left
- (fun g mr => Regset.fold (fun g r => add_interf_mreg r mr g) live g)
+ (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g)
destroyed g.
Fixpoint add_prefs_call