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 /cfrontend/PrintClight.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 'cfrontend/PrintClight.ml')
-rw-r--r-- | cfrontend/PrintClight.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ad6887c9..306224ba 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -231,17 +231,17 @@ let print_function p id f = f.fn_return); fprintf p "@[<v 2>{@ "; List.iter - (fun (Coq_pair(id, ty)) -> + (fun (id, ty) -> fprintf p "%s;@ " (name_cdecl (extern_atom id) ty)) f.fn_vars; List.iter - (fun (Coq_pair(id, ty)) -> + (fun (id, ty) -> fprintf p "register %s;@ " (name_cdecl (temp_name id) ty)) f.fn_temps; print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p (Coq_pair(id, fd)) = +let print_fundef p (id, fd) = match fd with | External(_, args, res) -> fprintf p "extern %s;@ @ " @@ -314,17 +314,17 @@ and collect_cases = function let collect_function f = collect_type f.fn_return; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars; - List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_temps; + List.iter (fun (id, ty) -> collect_type ty) f.fn_params; + List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; + List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; collect_stmt f.fn_body -let collect_fundef (Coq_pair(id, fd)) = +let collect_fundef (id, fd) = match fd with | External(_, args, res) -> collect_type_list args; collect_type res | Internal f -> collect_function f -let collect_globvar (Coq_pair(id, v)) = +let collect_globvar (id, v) = collect_type v.gvar_info let collect_program p = |