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 /arm | |
| parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
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 'arm')
| -rw-r--r-- | arm/PrintAsm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 50b585e..a616cc2 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -201,7 +201,7 @@ let call_helper oc fn dst arg1 arg2 = let moves = Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in List.iter - (fun (Coq_pair(s, d)) -> + (fun (s, d) -> fprintf oc " mov %a, %a\n" ireg d ireg s) moves; (* Call the helper function *) @@ -689,7 +689,7 @@ let print_function oc name fn = fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name -let print_fundef oc (Coq_pair(name, defn)) = +let print_fundef oc (name, defn) = match defn with | Internal code -> print_function oc name code @@ -729,7 +729,7 @@ let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) -let print_var oc (Coq_pair(name, v)) = +let print_var oc (name, v) = match v.gvar_init with | [] -> () | _ -> |