diff options
Diffstat (limited to 'backend/Coloringaux.mli')
| -rw-r--r-- | backend/Coloringaux.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Coloringaux.mli b/backend/Coloringaux.mli index c5070f20..7597c7ca 100644 --- a/backend/Coloringaux.mli +++ b/backend/Coloringaux.mli @@ -18,3 +18,5 @@ open InterfGraph val graph_coloring: coq_function -> graph -> regenv -> Regset.t -> (reg -> loc) + +val reserved_registers: Machregs.mreg list ref |