summaryrefslogtreecommitdiff
path: root/backend/Coloringaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Coloringaux.ml')
-rw-r--r--backend/Coloringaux.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 2fce25e..ddd3094 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -12,8 +12,6 @@
open Camlcoq
open Datatypes
-open BinPos
-open BinInt
open AST
open Maps
open Registers
@@ -766,8 +764,8 @@ let rec reuse_slot conflicts n mvlist =
let find_slot conflicts typ =
let rec find curr =
let l = S(Local(curr, typ)) in
- if Locset.mem l conflicts then find (coq_Zsucc curr) else l
- in find Z0
+ if Locset.mem l conflicts then find (Z.succ curr) else l
+ in find Z.zero
let assign_color n =
let conflicts = ref Locset.empty in