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 /ia32/PrintAsm.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 'ia32/PrintAsm.ml')
-rw-r--r-- | ia32/PrintAsm.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index f48b8080..5ca56d72 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -114,7 +114,7 @@ let addressing oc (Addrmode(base, shift, cst)) = | Coq_inl n -> let n = camlint_of_coqint n in fprintf oc "%ld" n - | Coq_inr(Coq_pair(id, ofs)) -> + | Coq_inr(id, ofs) -> let ofs = camlint_of_coqint ofs in if ofs = 0l then symbol oc id @@ -123,8 +123,8 @@ let addressing oc (Addrmode(base, shift, cst)) = begin match base, shift with | None, None -> () | Some r1, None -> fprintf oc "(%a)" ireg r1 - | None, Some(Coq_pair(r2,sc)) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc - | Some r1, Some(Coq_pair(r2,sc)) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc + | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc + | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc end let name_of_condition = function @@ -730,7 +730,7 @@ let print_function oc name code = jumptables := [] end -let print_fundef oc (Coq_pair(name, defn)) = +let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code | External ef -> () @@ -761,7 +761,7 @@ let print_init_data oc name id = else List.iter (print_init oc) id -let print_var oc (Coq_pair(name, v)) = +let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> |