diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
| commit | cdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch) | |
| tree | 8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /backend/Coloringaux.ml | |
| parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
| download | compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.tar.gz compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.zip | |
Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Coloringaux.ml')
| -rw-r--r-- | backend/Coloringaux.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index 34fab904..ab7d141f 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -410,11 +410,11 @@ let build g typenv spillcosts = n in (* Fill the adjacency set and the adjacency lists; compute the degrees. *) SetRegReg.fold - (fun (Coq_pair(r1, r2)) () -> + (fun (r1, r2) () -> addEdge (find_reg_node r1) (find_reg_node r2)) g.interf_reg_reg (); SetRegMreg.fold - (fun (Coq_pair(r1, mr2)) () -> + (fun (r1, mr2) () -> addEdge (find_reg_node r1) (find_mreg_node mr2)) g.interf_reg_mreg (); (* Process the moves and insert them in worklistMoves *) @@ -427,11 +427,11 @@ let build g typenv spillcosts = n2.movelist <- m :: n2.movelist; DLinkMove.insert m worklistMoves in SetRegReg.fold - (fun (Coq_pair(r1, r2)) () -> + (fun (r1, r2) () -> add_move (find_reg_node r1) (find_reg_node r2)) g.pref_reg_reg (); SetRegMreg.fold - (fun (Coq_pair(r1, mr2)) () -> + (fun (r1, mr2) () -> let r1' = find_reg_node r1 in if List.mem mr2 !allocatable_registers then add_move r1' (find_mreg_node mr2)) |