aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Machregsaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/Machregsaux.ml')
-rw-r--r--ia32/Machregsaux.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 3ec9596a..473e0602 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -22,12 +22,12 @@ let _ =
(fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
Machregs.register_names
-let scratch_register_names = []
+let is_scratch_register r = false
let name_of_register r =
try Some (Hashtbl.find register_names r) with Not_found -> None
let register_by_name s =
- Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
+ Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
let can_reserve_register r = Conventions1.is_callee_save r